the Final Simplification in the Base Case (Step 2)

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

Click on the link above to use the Axiom (EQUAL x x) = t