proposition: Theorem interp_mrec_as_interp {T} (c : itree _ T) : interp_mrec ctx c ≈ interp (mrecursive ctx) c.
proof: Proof. rewrite <- (tau_eutt (interp _ _)). revert_until T. ginit. pcofix CIH. intros. rewrite unfold_interp_mrec, unfold_interp. destruct (observe c); [| |destruct e]; simpl; eauto with paco. - gstep; repeat econstructor; eauto. - gstep; constructor; eauto with paco. - rewrite interp_mrec_bind. unfold mrec. gstep; constructor. guclo eqit_clo_bind; econstructor; [reflexivity|]. intros ? _ []; eauto with paco. - rewrite tau_euttge. unfold ITree.trigger, case_; simpl. rewrite bind_vis. gstep. constructor. intros; red. rewrite bind_ret_l. rewrite tau_euttge. auto with paco. 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)