The one place for your designs
To enable design management, you'll need to meet the requirements. If you need help, reach out to our support team for assistance.
Consider adding `iEnough` variants of `iAssert` ?
Something like:
Tactic Notation "iEnough" open_constr(Q) "with" constr(Hs) "as" constr(pat) :=
iAssert Q with Hs as pat; first last.
Tactic Notation "iEnough" open_constr(Q) "as" constr(pat) :=
iAssert Q as pat; first last.The point is just readability, and adding all the overloads is probably not worth it, but maybe this would change with an Ltac2 proofmode?