the Simplification of the Induction Conclusion (Step 8)

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

Click on the link above to expand the definition of APP here. This time, we'll do the whole expansion at once, including the simplification of the resulting IF. This is how ACL2 actually does it.