the Final Simplification in the Base Case (Step 3)

Subgoal *1/1'
(IMPLIES (NOT (CONSP A))
         T)

Now that its conclusion is identically T the IMPLIES will simplify to T (not shown) and we are done with Subgoal *1/1'.

You may click here to return to the main proof.