Reformatted code a bit
Changed primitive to natural numbers; added support for a local binding construct
Got type-checking application right (no correctness proof)