proposition: Lemma eutt_inv_bind_tau: forall {E A B} (ma : itree E A) (kab : A -> itree E B) (t: itree E B), ITree.bind ma kab ≈ Tau t -> (exists (ma' : itree E A), ma ≈ Tau ma' /\ ITree.bind ma' kab ≈ t) \/ (exists (a : A), ma ≈ Ret a /\ kab a ≈ Tau t).
proof: Proof. intros. apply eqit_inv_bind_tau. auto. Qed.
imports: Coq(Structures.Orders Program Setoid Morphisms Relations) Paco(paco) ITree(Basics.Basics Basics.Utils Basics.HeterogeneousRelations Core.ITreeDefinition Eq.Paco2 Eq.Shallow)