proposition: Lemma interp_fail_bind : forall {X Y E F} (t : itree _ X) (k : X -> itree _ Y) (h : E ~> failT (itree F)), interp_fail h (ITree.bind t k) ≅ ITree.bind (interp_fail h t) (fun mx => match mx with | None => ret None | Some x => interp_fail h (k x) end).
proof: Proof. intros X Y E F; ginit; pcofix CIH; intros. rewrite unfold_bind. rewrite (unfold_interp_fail h t). destruct (observe t) eqn:EQ; cbn. - rewrite bind_ret_l. apply reflexivity. - cbn. 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)