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