proposition: Lemma eutt_inv_bind_ret: forall {E A B} (ma : itree E A) (kb : A -> itree E B) b, ITree.bind ma kb ≈ Ret b -> exists a, ma ≈ Ret a /\ kb a ≈ Ret b.
proof: Proof. intros; apply eqit_inv_bind_ret; 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)