この記事はTppMark11の問題をCoqでやってみたという内容である。問題はこちら: docs.google.com 命題論理式と同値であることの定義 命題論理式の定義 Inductive Term := | Var(v : Var.T) | Neg(t : Term) | And(t1: Term)(t2: Term) | Or(t1: Term)(t2: Ter…