T258
(forall ?X (<=> (F ?X (a ?X)) (exists ?Y (and (forall ?Z (=> (F ?Z ?Y) (F ?Z (a ?X)))) (F ?X ?Y)))))
Proof Trace