proposition: Lemma may_converge_Ret_inv E (A : Type) (a a' : A) : may_converge (E := E) a (Ret a') -> a = a'.
proof: Proof. intros. inversion H. - apply eutt_inv_Ret in H0. auto. - apply eqit_inv in H0; cbn in H0; contradiction. Qed.
imports: Coq(Setoid Morphisms RelationClasses) Paco(paco) ITree(Axioms Basics Core.ITreeDefinition Eq.Eqit Eq.Shallow)