proposition: Lemma transLleU: transL <3= transU RR.
proof: Proof. intros. destruct PR. econstructor; eauto. reflexivity. auto_ctrans. Qed.
imports: Coq(Setoid Morphisms Relations) Paco(paco) ITree(Basics.Utils Core.ITreeDefinition Eq.Eqit Eq.Paco2 Eq.Shallow)