proposition: Lemma eutt_inv_Ret_r {E R} (t1: itree E R) (r2: R): t1 ≈ (Ret r2) -> t1 ≳ (Ret r2).
proof: Proof. intros Heutt. punfold Heutt; red in Heutt; cbn in Heutt. rewrite itree_eta. remember (RetF r2) as ot2. induction Heutt; intros; try discriminate. - inv Heqot2. reflexivity. - inv Heqot2. rewrite tau_euttge. rewrite itree_eta. now apply IHHeutt. Qed.
imports: Coq(Structures.Orders Program Setoid Morphisms Relations) Paco(paco) ITree(Basics.Basics Basics.Utils Basics.HeterogeneousRelations Core.ITreeDefinition Eq.Paco2 Eq.Shallow)