proposition: Lemma euttG_drop rH rL gL gH t1 t2: euttG rH rH rH gH t1 t2 -> euttG rH rL gL gH t1 t2.
proof: Proof. intros. apply euttG_gen. destruct H. econstructor. eapply gpaco2_mon; intros; eauto; [destruct PR|]; eauto using transU_id. Qed.
imports: Coq(Setoid Morphisms Relations) Paco(paco) ITree(Basics.Utils Core.ITreeDefinition Eq.Eqit Eq.Paco2 Eq.Shallow)