proposition: Lemma eqit_ret_gen {E R1 R2 RR} t v (IN: @eqit E R1 R2 RR true true t (Ret v)): eqit RR true false t (Ret v).
proof: Proof. punfold IN. pstep. red in IN |- *. simpl in *. remember (RetF v) as ot. hinduction IN before RR; intros; subst; try inv Heqot; eauto with itree. Qed.
imports: Coq(Setoid Morphisms Relations) Paco(paco) ITree(Basics.Utils Core.ITreeDefinition Eq.Eqit Eq.Paco2 Eq.Shallow)