proposition: Lemma eqit_flip {E R1 R2} (RR : R1 -> R2 -> Prop) b1 b2: forall (u : itree E R1) (v : itree E R2), eqit (flip RR) b2 b1 v u -> eqit RR b1 b2 u v.
proof: Proof. pcofix self; pstep. intros u v euv. punfold euv. red in euv |- *. induction euv; pclearbot; eauto 7 with paco itree. Qed.
imports: Coq(Structures.Orders Program Setoid Morphisms Relations) Paco(paco) ITree(Basics.Basics Basics.Utils Basics.HeterogeneousRelations Core.ITreeDefinition Eq.Paco2 Eq.Shallow)