The Rules used in the Associativity of App Proof

Note that under Rules we list the runes of all the rules used in the proof. This list says that we used the rewrite rules CAR-CONS and CDR-CONS, the definitions of the functions NOT, ENDP and APP, and primitive type reasoning (which is how we simplified the IF and EQUAL terms).

For what it is worth, IMPLIES and AND are actually macros that are expanded into IF expressions before the proof ever begins. The use of macros is not reported among the rules.