proposition: Lemma interp_fail_ret : forall {X E F} (h : E ~> failT (itree F)) (x : X), interp_fail h (Ret x) ≅ ret (m := failT (itree F)) x.
proof: Proof. intros; 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)