T301
(= x x)
Proof Trace