proposition: Lemma transD_mon r1 r2 t1 t2 (IN: transD r1 t1 t2) (LE: r1 <2= r2): transD r2 t1 t2.
proof: Proof. eapply eqitC_mon, LE; eauto. Qed.
imports: Coq(Setoid Morphisms Relations) Paco(paco) ITree(Basics.Utils Core.ITreeDefinition Eq.Eqit Eq.Paco2 Eq.Shallow)