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?