補足：Falseのパターンマッチのextraction

パターンマッチができるってことは、extractionできるということである。
singleton definitionのパターンマッチの場合、実は非常に簡単で、そのパターンマッチ自体が消えて、結果だけが残る。
一方、empty definitionはそうも行かない。そもそもCoqのterm上は分岐がないのだ。
しかもFalse自体は述語なので消える運命にある。
ではどうなるのか？


結果はこれまた簡単、assert（やそれに類するもの）を使って異常状態であることを知らせる。
なぜなら、検証した結果としてはそこに来ることを想定していないわけだから。
というわけで、これでextractionも可能となり、すべてが丸く収まったわけである。


これで終わり？まだもうひとつある。でもそれはいつ書くか不明。