proposition: Lemma eqitree_inv_Ret {E R} r1 r2 : (Ret r1: itree E R) ≅ (Ret r2) -> r1 = r2.
proof: Proof. intros; eapply eqit_inv_Ret; eauto. Qed.
imports: Coq(Structures.Orders Program Setoid Morphisms Relations) Paco(paco) ITree(Basics.Basics Basics.Utils Basics.HeterogeneousRelations Core.ITreeDefinition Eq.Paco2 Eq.Shallow)