proposition: Lemma interp_fail_vis {E F : Type -> Type} {T U : Type} (e : E T) (k : T -> itree E U) (h : E ~> failT (itree F)) : interp_fail h (Vis e k) ≅ h T e >>= fun mx => match mx with | None => Ret None | Some x => Tau (interp_fail h (k x)) end.
proof: Proof. rewrite unfold_interp_fail. 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)