knuton/proof-theory — pull request #13 by yfyf (2012-10-20 10:47:09+00:00)
Title: Restrict \lambda_\Pi to well-typed terms

This is rather wordy, but I'm shifting now to cleaning up the part in untyped-lambda-calc and normals forms.