proposition: Lemma interp_bind {E F R S} (f : E ~> itree F) (t : itree E R) (k : R -> itree E S) : interp f (ITree.bind t k) ≅ ITree.bind (interp f t) (fun r => interp f (k r)).
proof: Proof. revert R t k. ginit. pcofix CIH; intros. rewrite unfold_bind, (unfold_interp t). destruct (observe t); cbn. - rewrite bind_ret_l. apply reflexivity. - rewrite bind_tau, !interp_tau. gstep. econstructor. eauto with paco. - rewrite interp_vis, bind_bind. guclo eqit_clo_bind; econstructor; try reflexivity. intros; subst. rewrite bind_tau. gstep; constructor; eauto with paco. Qed.
imports: Coq(Program Setoid Morphisms RelationClasses) Paco(paco) ITree(Basics.Basics Basics.Category Basics.CategoryKleisli Basics.CategoryKleisliFacts Core.ITreeDefinition Core.KTree Core.KTreeFacts Eq.Shallow Eq.Eqit Eq.UpToTaus Eq.Paco2 Indexed.Sum Indexed.Function Indexed.Relation Interp.Interp Interp.Handler Interp.TranslateFacts)