proposition: Lemma interp_failure_bind' : forall {X Y E F} (t : itree _ X) (k : X -> itree _ Y) (h : E ~> failT (itree F)), interp_fail h (bind t k) ≅ bind (interp_fail h t) (fun x => interp_fail h (k x)).
proof: Proof. intros X Y E F. cbn. ginit; pcofix CIH; intros. cbn in *. rewrite unfold_bind, (unfold_interp_fail _ t). destruct (observe t) eqn:EQ; cbn. - rewrite bind_ret_l. apply reflexivity. - rewrite bind_tau, !interp_fail_tau. gstep. econstructor; eauto with paco. - rewrite bind_bind, interp_fail_vis. guclo eqit_clo_bind; econstructor. reflexivity. intros [] ? <-; cbn. + rewrite bind_tau. gstep; constructor. ITree.fold_subst. auto with paco. + rewrite bind_ret_l. apply reflexivity. Qed.
imports: Coq(Morphisms) Paco(paco) ITree(Basics.Utils Basics.Basics Basics.Category Basics.CategoryKleisli Basics.HeterogeneousRelations Basics.Monad Core.ITreeDefinition Core.KTree Core.KTreeFacts Eq.Eqit Eq.UpToTaus Eq.Paco2 Indexed.Sum Interp.Interp Interp.InterpFacts Interp.RecursionFacts)