Subgoal *1/2' (IMPLIES (AND (CONSP A) (EQUAL (APP (APP (CDR A) B) C) (APP (CDR A) (APP B C)))) (EQUAL (CONS (CAR A) (APP (APP (CDR A) B) C)) (APP A (APP B C)))).
Click on the link above to expand the definition of
APP here. This time,
we'll do the whole expansion at once, including the simplification of the
IF. This is how ACL2 actually does it.