Coq proof scripts for type unicity for PCF May 2009.
The files must be compiled in this order:
Hybrid.v
spec_nat.v
tyunicity.v