proposition: Theorem unfold_interp_mrec_h {T} (t : itree _ T) : interp_mrec ctx (interp (case_ (C := Handler) ctx inr_) t) ≈ interp_mrec ctx t.
proof: Proof. rewrite <- tau_eutt. revert t. ginit; pcofix CIH. intros. rewrite (itree_eta t); destruct (observe t). - rewrite 2 unfold_interp_mrec; cbn; gstep; repeat constructor; auto with paco. - rewrite unfold_interp, 2 unfold_interp_mrec; cbn. gstep. constructor; auto with paco. - rewrite interp_vis. rewrite (unfold_interp_mrec _ (Vis _ _)). destruct e; cbn. + rewrite 2 interp_mrec_bind. gstep; constructor. guclo eqit_clo_bind; econstructor; [reflexivity|]. intros ? _ []; rewrite unfold_interp_mrec; cbn; auto with paco. + unfold inr_, Handler.Inr_sum1_Handler, Handler.Handler.inr_, Handler.Handler.htrigger. rewrite bind_trigger, unfold_interp_mrec; cbn. rewrite tau_euttge. gstep; constructor. intros; red. gstep; constructor. rewrite unfold_interp_mrec; cbn. 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)