[POPLmark] New solution to Part 1A

[Adam Chlipala]

I've put up a new solution to Part 1A of the original challenge at:
	http://www.cs.berkeley.edu/~adamc/poplmark/

It's implemented in Coq and uses the locally-nameless approach.  I've 
tried to make the main solution file very human readable, by developing 
a separate library of facts about typing contexts and by using 
automation for most of the proof generation.

There's more information on the page that I linked.