proposition: Lemma euttge_trans_clo_mon r1 r2 t1 t2 (IN : euttge_trans_clo r1 t1 t2) (LE : r1 <2= r2) : euttge_trans_clo r2 t1 t2.
proof: Proof. destruct IN; econstructor; eauto. Qed.
imports: Coq(Morphisms ) ExtLib(Structures.Monad) ITree(Basics.Utils Axioms ITree Eq Basics ) Paco(paco)