the Final Simplification in the Base Case (Step 1)

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

Click on the link above to expand the definition of APP. Again, we come out through the false branch because of the hypothesis.