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
APP to its false branch this time.