proposition: Lemma eqitree_inv_bind_vis: forall {A B E X} (ma : itree E A) (kab : A -> itree E B) (e : E X) (kxb : X -> itree E B), ITree.bind ma kab ≅ Vis e kxb -> (exists (kca : X -> itree E A), (ma ≅ Vis e kca) /\ forall (x:X), (ITree.bind (kca x) kab) ≅ (kxb x)) \/ (exists (a : A), (ma ≅ Ret a) /\ (kab a ≅ Vis e kxb)).
proof: Proof. intros. apply eqit_inv_bind_vis. 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)