J016
(forall ?X (exists ?Y (<=> (F ?X) (F ?Y))))
Proof Trace