>>984
具体的に説明するか

Coq証明系の存在証明をCoqで書いて
プログラムとして抽出すればいいってこと

カリー＝ハワード同型対応
https://ja.wikipedia.org/wiki/%E3%82%AB%E3%83%AA%E3%83%BC%EF%BC%9D%E3%83%8F%E3%83%AF%E3%83%BC%E3%83%89%E5%90%8C%E5%9E%8B%E5%AF%BE%E5%BF%9C