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
This time, we'll do the whole expansion at once, including the
simplification of the resulting
IF. This is how ACL2 actually