proposition: Lemma eutt_inv_Ret_l {E R} (r1: R) (t2: itree E R): (Ret r1) ≈ t2 -> t2 ≳ (Ret r1).
proof: Proof. intros Heutt. punfold Heutt; red in Heutt; cbn in Heutt. rewrite itree_eta. remember (RetF r1) as ot1. induction Heutt; intros; try discriminate. - inv Heqot1. reflexivity. - inv Heqot1. 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)