proposition: Lemma euttG_gen rH rL gL gH: euttG rH rL (gL \2/ (transU RR rH \2/ rL)) gH <2= euttG rH rL gL gH.
proof: Proof. intros. destruct PR. econstructor. eapply gpaco2_gen_guard. eauto. Qed.
imports: Coq(Setoid Morphisms Relations) Paco(paco) ITree(Basics.Utils Core.ITreeDefinition Eq.Eqit Eq.Paco2 Eq.Shallow)