KM158-6
(=> (forall ?X (G ?X ?X)) (forall ?X (G a ?X)))
Proof Trace