proposition: Lemma transU_flip r: flip (transU (flip RR) (flip r)) <2= @transU E R1 R2 RR r.
proof: Proof. unfold flip. intros. destruct PR. econstructor; eauto. Qed.
imports: Coq(Setoid Morphisms Relations) Paco(paco) ITree(Basics.Utils Core.ITreeDefinition Eq.Eqit Eq.Paco2 Eq.Shallow)