iAssert ... as %X should get all assumptions
When I write
iAssert ... as %X, it is syntactically clear that I am proving sth. persistent (even pure). Still, I have to add
with [#] to be allowed to use all assumptions. Wouldn't it make sense to do that automatically? IIRC we are doing sth. like that with ´iDestruct ... as %X`.