<div dir="ltr"><div>Hi all:</div><div><br></div><div>   I find myself sometimes wanting to work on two expressions in a single hole at the same time. Typically one is going to be in an argument to the other but they have to fit together in a certain way that I find hard to predict without working through the details of each separately. Is there some facility for doing that or some trick that folks use in similar situations? I tried just separating them with a comma which works sometimes but not always (when the pair constructor is in scope) as the dependency sometimes gets in the way.</div><div><br></div><div>One example of this is `trans` -- when you're working on an equality proof and you want to tweak both of them to get the thing that'll eventually end up in the middle. (With trans specifically, actually, I've gotten used to it enough that I don't actually need the help anymore, but hopefully it makes the request clearer.)</div><div><br></div><div>tia,</div><div>Robby</div><div><br></div></div>