Overview of the Simplification of the Base Case to T

Subgoal *1/1
(IMPLIES (ENDP A)
         (EQUAL (APP (APP A B) C)
                (APP A (APP B C)))).


By the simple :definition ENDP we reduce the conjecture to


Subgoal *1/1'
(IMPLIES (NOT (CONSP A))
         (EQUAL (APP (APP A B) C)
                (APP A (APP B C)))).


But simplification reduces this to T, using the :definition APP and
primitive type reasoning.