J023
(=> (forall ?X (or (= ?X a) (= ?X b))) (or (forall ?X (= ?X a)) (forall ?X (= ?X b))))
Proof Trace