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
But we know the test
(CONSP A) is true, by the first hypothesis.
Click on the link above to replace the test by
this step and several subsequent ones are done during the simplification
of the body of
APP but we want to illustrate the basic principles of
simplification without bothering with every detail.