You could take a look at Coquand (2002) “A formalised proof of the soundness and completeness of a simply typed lambda-calculus with explicit substitutions”. h

You could take a look at Coquand (2002) “A formalised proof of the soundness and completeness of a simply typed lambda-calculus with explicit substitutions”. https://www.dropbox.com/s/xmj7yv1i1moe0ag/Coquand2002.pdf https://www.dropbox.com/s/xmj7yv1i1moe0ag/Coquand2002.pdf Drop in to #dependent on Freenode IRC, and let’s chat.