PA102a
Premises:
(forall ?X (= (* (1+ 0) ?X) ?X))
Conclusion:
(= (* (1+ 0) (1+ (1+ 0))) (1+ (1+ 0)))
Proof Trace