えーと、TAPLの3.2.5をCoqを使って、証明しようと思ってたところです。TAPLの3.2.5を証明するには、Coqで実装する方法を知らないと出来ないのでした。なので、実装方法を知らねばならず、4章の内容を知らないと出来ない事をやろうとしてますと。しかも、Coq…