T327
(=> (forall ?X (= (a ?X) (b ?X))) (<=> (exists ?X (f (a ?X))) (exists ?X (f (b ?X)))))
Proof Trace