J010
(=> (forall ?X (P ?X ?X)) (exists ?X (forall ?Y (P ?X ?Y))))
Proof Trace