fact: Definition with_mmatch: forall {P:Prop}, M P := mfix1 f (P: Prop) : M P := mmatch P as P' return M (P':Prop) with | True => M.ret I | [? Q R] Q /\ R => r1 <- f Q; r2 <- f R; M.ret (conj r1 r2) end.
imports: Mtac2(Mtac2 DecomposeApp)