proposition: Lemma eqit_inv_Ret {E R1 R2 RR} b1 b2 r1 r2 : @eqit E R1 R2 RR b1 b2 (Ret r1) (Ret r2) -> RR r1 r2.
proof: Proof. intros. punfold H. inv H. eauto. Qed.
imports: Coq(Structures.Orders Program Setoid Morphisms Relations) Paco(paco) ITree(Basics.Basics Basics.Utils Basics.HeterogeneousRelations Core.ITreeDefinition Eq.Paco2 Eq.Shallow)