練習題材としてSTLC(Simple Typed Lambda Calculus)を使うことにした。 http://www.cs.virginia.edu/~wh5a/coq/SimpTypLCalc/STLC.v ：coqコード http://citeseer.ist.psu.edu/742197.html : 上とほぼ同じものについて書いてある論文 以下は、このSTLC.vが読…