相変わらずCoq書いてるけど進歩ないすなぁ。Coqの特徴ってのはまあ、Inductive型が使えて帰納法ができてハッピーというアレなんだけど、あまりそこに到達していないとこがなんとも。 証明中にやりたくてもできないという知識的欠陥で、Arithmeticの周辺でラ…