The End of the Proof of the Associativity of App

That completes the proof of *1.


Q.E.D.


Summary
Form:  ( DEFTHM ASSOCIATIVITY-OF-APP ...)
Rules: ((:REWRITE CDR-CONS)
        (:REWRITE CAR-CONS)
        (:DEFINITION NOT)
        (:DEFINITION ENDP)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:DEFINITION APP))
Warnings:  None
Time:  0.27 seconds (prove: 0.10, print: 0.05, other: 0.12)
 ASSOCIATIVITY-OF-APP