proposition: Lemma euttG_transU rH rL gL gH t1 t2: transU RR (euttG rH rH rH gH) t1 t2 -> euttG rH rL gL gH t1 t2.
proof: Proof. intros. apply euttG_gen. cut (gupaco2 (eqit_ RR true true (euttVC RR gH)) (transD RR) (transU RR rH) t1 t2). { intros. econstructor. eapply gpaco2_mon; eauto. } eapply euttG_transU_aux; eauto using transU_compose. eapply transU_mon; eauto. intros. destruct PR. eapply gpaco2_mon; eauto; intros; repeat destruct PR as [PR|PR]; eauto using transU_id. Qed.
imports: Coq(Setoid Morphisms Relations) Paco(paco) ITree(Basics.Utils Core.ITreeDefinition Eq.Eqit Eq.Paco2 Eq.Shallow)