the Simplification of the Induction Conclusion (Step 11)

Subgoal *1/2'
(IMPLIES (AND (CONSP A)
              (EQUAL (APP (APP (CDR A) B) C)
                     (APP (CDR A) (APP B C))))
         T)

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.