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
resulting IF
. This is how ACL2 actually does it.