T314
(<=> (f x y) (forall ?Z (forall ?W (=> (and (= ?Z x) (= ?W y)) (f ?Z ?W)))))
Proof Trace