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