一月の終わりごろから Coq で遊んでいます。あまり自明でないこともだんだんできるようになってきた気がしますが，なにかがわかるようになってくるということとなにかがわからないと気付くこととはたいていの場合同時に起こることのようです。tactic が何を…