proposition: Lemma euttVC_compat gH: compose transD (euttVC gH) <3= compose (euttVC gH) transD.
proof: Proof. intros. gclo. eapply transD_mon; eauto. intros. eapply gupaco2_mon; eauto. intros. eapply transU_mon; eauto. intros. destruct PR2; eauto. left. econstructor; try reflexivity; auto_ctrans. Qed.
imports: Coq(Setoid Morphisms Relations) Paco(paco) ITree(Basics.Utils Core.ITreeDefinition Eq.Eqit Eq.Paco2 Eq.Shallow)