proposition: Lemma euttVC_transL gH r: transL (euttVC RR gH r) <2= euttVC RR gH r.
proof: Proof. intros. eapply transL_closed; eauto using transU_compose, transLleU, transDleU with paco. Qed.
imports: Coq(Setoid Morphisms Relations) Paco(paco) ITree(Basics.Utils Core.ITreeDefinition Eq.Eqit Eq.Paco2 Eq.Shallow)