the Final Simplification in the Base Case (Step 0)

Subgoal *1/1'
(IMPLIES (NOT (CONSP A))
         (EQUAL (APP (APP A B) C)
                (APP A (APP B C)))).

Click on the link above to replace (APP A B) by its definition. Note that the hypothesis (NOT (CONSP A)) allows us to simplify the IF in APP to its false branch this time.