## 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.