proposition: Lemma interp_fail_tau {E F R} {f : E ~> failT (itree F)} (t: itree E R): eq_itree eq (interp_fail f (Tau t)) (Tau (interp_fail f t)).
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)