Subgoal *1/2' (IMPLIES (AND (CONSP A) (EQUAL (APP (APP (CDR A) B) C) (APP (CDR A) (APP B C)))) (EQUAL (APP (IF (CONSP A) (CONS (CAR A) (APP (CDR A) B)) B) C) (APP A (APP B C)))).
Note that the
IF expression above is the simplified body of
we know the test
(CONSP A) is true, by the first hypothesis. Click on
the link above to replace the test by
T. Actually this step and several
subsequent ones are done during the simplification of the body of
we want to illustrate the basic principles of simplification without
bothering with every detail.