proposition: Theorem interp_mrec_bind {U T} (t : itree _ U) (k : U -> itree _ T) : interp_mrec ctx (ITree.bind t k) ≅ ITree.bind (interp_mrec ctx t) (fun x => interp_mrec ctx (k x)).
proof: Proof. revert t k; ginit. pcofix CIH; intros. rewrite (unfold_interp_mrec _ t). rewrite (unfold_bind t). destruct (observe t); cbn; [| |destruct e]; autorewrite with itree. 1: apply reflexivity. all: rewrite unfold_interp_mrec; ITree.fold_subst. all: try (gstep; econstructor; eauto with paco). - rewrite <- bind_bind; eauto with paco. - intros. red. rewrite bind_tau. gstep; constructor; 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)