T315
(<=> (f x y) (exists ?Z (exists ?W (and (= ?Z x) (= ?W y) (f ?Z ?W)))))
Proof Trace