proposition: Theorem mrec_as_interp {T} (d : D T) : mrec ctx d ≈ interp (mrecursive ctx) (ctx _ d).
proof: Proof. apply interp_mrec_as_interp. 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)