[TAPL][Coq] Chapter 3: Boolean Expression

TAPLのChapter 3のBoolean式の部分に付いてCoqで証明してみました。
コードは http://ideone.com/COzSO に公開しています。