proposition: Lemma interp_mrecursive {T} (d : D T) : interp (mrecursive ctx) (trigger_inl1 d) ≈ mrec ctx d.
proof: Proof. unfold mrecursive. unfold trigger_inl1. rewrite interp_trigger. cbn. reflexivity. Qed.
imports: Paco.paco Coq(Program.Tactics Setoid Morphisms) ITree(Basics.Utils Basics.Category Basics.Basics Basics.Function Core.ITreeDefinition Core.KTree Eq.Eqit Eq.UpToTaus Eq.Paco2 Indexed.Sum Indexed.Function Indexed.Relation Interp.Handler Interp.Interp Interp.InterpFacts Interp.Recursion)