Coq のカリー・ハワード同型周辺についてメモ．間違いあればご指摘ください．Coq と CoCCoq は元々，Thierry Coquand 氏により提案された Calculus of Cons…