proposition: Lemma euttG_vis_gen rH rL gL gH u1 (e1: E u1) u2 (e2 : E u2) k1 k2 (p : u1 = u2) : eqeq E p e1 e2 -> pweqeq (euttG gH gH gH gH) p k1 k2 -> euttG rH rL gL gH (Vis e1 k1) (Vis e2 k2).
proof: Proof. econstructor. gstep. apply (eqitF_VisF_gen p); auto. destruct p; cbn in *; intros. specialize (H0 x). destruct H0. 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)