proposition: Lemma euttVC_transU gH r (CLOR: transU RR r <2= r): transU RR (euttVC RR gH r) <2= @euttVC E _ _ RR gH r.
proof: Proof. intros. destruct PR. eapply euttVC_transL; eauto using transLleU, transDleU with paco. econstructor; eauto. eapply euttVC_flip. unfold flip. eapply euttVC_transL; eauto using transLleU, transDleU, transU_flip with paco. econstructor; eauto. apply euttVC_flip. eauto. Qed.
imports: Coq(Setoid Morphisms Relations) Paco(paco) ITree(Basics.Utils Core.ITreeDefinition Eq.Eqit Eq.Paco2 Eq.Shallow)