消除通用量词基本上只是应用, 所以要用w替换w,只需将x应用于pw_o y z的实例h2即可。
theorem prelim': ? x y z : A, g_o x y �� pw_o y z �� g_o x z := begin intros, cases a with h1 h2, cases h2 x with h3 _, sorry end