I was able to fix all the basic results, and cleaned up the dirty
proofs.  I fixed the issues by eliminated the kinding conversion lemma
all together. It was only needed in one case of the regularity lemma,
which could be avoided by adding a kinding assumption to the conv
rule. I deemed it simpler than trying to get kinding conversion
working.

I am not working through the rest of the proofs to make sure they work.

git-svn-id: https://svn.divms.uiowa.edu/repos/clc/reports/harley_thesis@17185 bd178f5f-7bea-4014-844f-495ca19b8805
Preservation was missing the case for when a recursion is applied to a
value.  Even worse this case depends on two inversion lemmas that are
very much like the inversion lemma we needed for lambdas.  Luckily,
these were so alike the proofs were easy.  So type preservation is
looking good now.

git-svn-id: https://svn.divms.uiowa.edu/repos/clc/reports/harley_thesis@17188 bd178f5f-7bea-4014-844f-495ca19b8805
Going through consistency now.  This proof depends on left-to-right CBV,
but I had defined right-to-left CBV.  Fixed it.

git-svn-id: https://svn.divms.uiowa.edu/repos/clc/reports/harley_thesis@17189 bd178f5f-7bea-4014-844f-495ca19b8805
The "substitution for kinding and typing" lemma was wrong.  I replaced
it with a new lemma called Well-formed substitution for typing.  It
holds by straightforward induction.  The proof is pretty boring so I
only give a few cases.

git-svn-id: https://svn.divms.uiowa.edu/repos/clc/reports/harley_thesis@17192 bd178f5f-7bea-4014-844f-495ca19b8805
Okay, everything up to type soundness looks good.

git-svn-id: https://svn.divms.uiowa.edu/repos/clc/reports/harley_thesis@17193 bd178f5f-7bea-4014-844f-495ca19b8805
Finally, type soundness now looks good.  I think all the results are
good to go.

git-svn-id: https://svn.divms.uiowa.edu/repos/clc/reports/harley_thesis@17194 bd178f5f-7bea-4014-844f-495ca19b8805
Some rewording.

git-svn-id: https://svn.divms.uiowa.edu/repos/clc/reports/harley_thesis@17199 bd178f5f-7bea-4014-844f-495ca19b8805
Merge branch 'clc'