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