proposition: Lemma eutt_Ret : forall E (R1 R2 : Type) (RR : R1 -> R2 -> Prop) r1 r2, RR r1 r2 <-> eutt (E := E) RR (Ret r1) (Ret r2).
proof: Proof. intros; apply eqit_Ret. Qed.
imports: Coq(Setoid Morphisms Relations) Paco(paco) ITree(Basics.Utils Core.ITreeDefinition Eq.Eqit Eq.Paco2 Eq.Shallow)