proposition: Lemma euttG_vis: forall rH rL gL gH u (e: E u) k1 k2, (forall v, euttG gH gH gH gH (k1 v) (k2 v)) -> euttG rH rL gL gH (Vis e k1) (Vis e k2).
proof: Proof. econstructor. gstep. econstructor. intros. specialize (H v). destruct H. apply euttVC_gen. econstructor; auto_ctrans_eq; try reflexivity. eapply gpaco2_mon_gen; eauto; intros; repeat destruct PR as [PR|PR]; eauto using gpaco2_clo, transDleU, transU_mon with paco. Qed.
imports: Coq(Setoid Morphisms Relations) Paco(paco) ITree(Basics.Utils Core.ITreeDefinition Eq.Eqit Eq.Paco2 Eq.Shallow)