proposition: Lemma interp_fail_trigger {E F : Type -> Type} {R : Type} (e : E R) (f : E ~> failT (itree F)) : interp_fail f (ITree.trigger e) ≈ f _ e.
proof: Proof. unfold ITree.trigger. rewrite interp_fail_vis. match goal with |- ?y ≈ ?x => remember y; rewrite <- (bind_ret_r x); subst end. eapply eutt_eq_bind. intros []; try reflexivity; rewrite interp_fail_ret,tau_eutt. 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)