Overview of the Simplification of the Induction Step to T

Subgoal *1/2
(IMPLIES (AND (NOT (ENDP A))
              (EQUAL (APP (APP (CDR A) B) C)
                     (APP (CDR A) (APP B C))))
         (EQUAL (APP (APP A B) C)
                (APP A (APP B C)))).


By the simple :definition ENDP we reduce the conjecture to


Subgoal *1/2'
(IMPLIES (AND (CONSP A)
              (EQUAL (APP (APP (CDR A) B) C)
                     (APP (CDR A) (APP B C))))
         (EQUAL (APP (APP A B) C)
                (APP A (APP B C)))).


But simplification reduces this to T, using the :definition APP, the
:rewrite rules CDR-CONS and CAR-CONS and primitive type reasoning.