The Expansion of ENDP in the Induction Step (Step 0)

Subgoal *1/2
(IMPLIES (AND (NOT (ENDP A))
              (EQUAL (APP (APP (CDR A) B) C)
                     (APP (CDR A) (APP B C))))
         (EQUAL (APP (APP A B) C)
                (APP A (APP B C)))).

Click on the link above (the open parenthesis before ENDP) to replace (ENDP A) by its definition.