proposition: Lemma eqit_Ret b1 b2 (r1 : R1) (r2 : R2) : RR r1 r2 <-> @eqit E _ _ RR b1 b2 (Ret r1) (Ret r2).
proof: Proof. split; intros H. - pstep. constructor; auto. - punfold H. inversion H; subst; auto. Qed.
imports: Coq(Structures.Orders Program Setoid Morphisms Relations) Paco(paco) ITree(Basics.Basics Basics.Utils Basics.HeterogeneousRelations Core.ITreeDefinition Eq.Paco2 Eq.Shallow)