Minimal usable implementation.

This version has enough functionality for languages with moderately interesting binding structure. For example, see the unbound-generics branch of pi-forall.