Equivalence theorem for CCC's and simply-typed lambda-calculi.

pf.dvi       : a "paper proof" of the theorem.

ccc.elf      : (static) definition of cartesian closed categories
lambda.elf   : (static) definition of simply-typed lambda-calculus

catlem.elf   : a few categorical lemmas
cong.elf     : general congruence lemma for lambda-terms

abs-env.elf  : translation from lambda-terms to ccc combinators
subext.elf   : the substitution extension lemma
eqpres1.elf  : preservation of beta-eta-pairing equality

conc.elf     : translation from ccc combinators to lambda-terms
eqpres2.elf  : preservation of ccc equality

inv1.elf     : translation lambda->ccc->lamda is identity
inv2.elf     : translation ccc->lambda->ccc is identity
refl.elf     : equality-reflection corollary (both ways)

examples.quy : sample queries
