proposition: Lemma transD_transL r: transD RR (transL r) <2= transL (transD RR r).
proof: Proof. intros. destruct PR, REL. econstructor; [|econstructor|]; try apply EQR. - eapply eqit_trans. + apply euttge_sub_eutt. eauto. + eauto. - reflexivity. - eauto. - auto_ctrans. - auto_ctrans. - auto_ctrans. Qed.
imports: Coq(Setoid Morphisms Relations) Paco(paco) ITree(Basics.Utils Core.ITreeDefinition Eq.Eqit Eq.Paco2 Eq.Shallow)