the Simplification of the Induction Conclusion (Step 1)

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

Note that the IF expression above is the simplified body of APP. But we know the test (CONSP A) is true, by the first hypothesis. Click on the link above to replace the test by T. Actually this step and several subsequent ones are done during the simplification of the body of APP but we want to illustrate the basic principles of simplification without bothering with every detail.