proposition: Lemma euttG_transU_aux gH r (CLOR: transU RR r <2= r): transU RR (gupaco2 (eqit_ RR true true (euttVC RR gH)) (transD RR) r) <2= gupaco2 (@eqit_ E R1 R2 RR true true (euttVC RR gH)) (transD RR) r.
proof: Proof. intros. destruct PR. eapply transL_closed; eauto using euttVC_transL, transLleU, transDleU with paco. econstructor; eauto. apply euttG_flip. unfold flip. eapply transL_closed; [ eauto using euttVC_transL, transLleU, transDleU, transU_flip with paco itree .. | ]. econstructor; eauto using euttG_flip with itree. Qed.
imports: Coq(Setoid Morphisms Relations) Paco(paco) ITree(Basics.Utils Core.ITreeDefinition Eq.Eqit Eq.Paco2 Eq.Shallow)