WORK IN PROGRESS --- PLEASE DO NOT DISTRIBUTE

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)

load.sml	-- SML wrapper to load Elf files
examples.quy	-- sample queries