proposition: Lemma unfold_interp_mrec R (t : itree (D +' E) R) : interp_mrec ctx t ≅ _interp_mrec (observe t).
proof: Proof. unfold interp_mrec. rewrite unfold_iter. destruct observe; cbn. - rewrite bind_ret_l; reflexivity. - rewrite bind_ret_l; reflexivity. - destruct e; cbn. + rewrite bind_ret_l; reflexivity. + rewrite bind_vis. pstep; constructor. intros. left. rewrite bind_ret_l. apply 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)