The Simplification of the Induction Conclusion (Step 11)
(IMPLIES (AND (CONSP A)
(EQUAL (APP (APP (CDR A) B) C)
(APP (CDR A) (APP B C))))
Click on the link above to use the definition of IMPLIES. Since the
conclusion of the implication is now identically T, the implication
simplifies to T.