proposition: Lemma euttVC_mon gH: monotone2 (euttVC gH).
proof: Proof. red; intros. eapply gupaco2_mon; eauto. intros. eapply transU_mon; eauto. intros. destruct PR0; eauto. Qed.
imports: Coq(Setoid Morphisms Relations) Paco(paco) ITree(Basics.Utils Core.ITreeDefinition Eq.Eqit Eq.Paco2 Eq.Shallow)