proposition: Lemma interp_mrecursive : forall {D E T} (ctx : D ~> itree (D +' E)) (d : D T), interp (mrecursive ctx) (trigger_inl1 d) ≈ mrec ctx d.
proof: Proof. intros; rewrite ITree.Interp.RecursionFacts.interp_mrecursive. reflexivity. Qed.
imports: Coq(Setoid Morphisms) ITree(Eq.Shallow) ITree.Core.ITreeDefinition ITree.Basics.Basics ITree.Indexed.Sum ITree.Interp.Interp ITree.Interp.Recursion ITree(Eq.Eqit Eq.UpToTaus Interp.InterpFacts Interp.RecursionFacts)