この記事はTheorem Prover Advent Calendar 2016 12日目の記事です。 この記事は定理証明初心者向けの記事です。 普段から依存型を用いた定理証明をされている方は読む必要がありません。 "coherence condition"と呼ばれる条件があり、訳すと「一貫性条件」…