最近Coqをかいていて、まぁ自分は基本姿勢として「CoqにはProof Assistantの方向性として共感できないのでもっとよいものが出てきて早く駆逐してほしい」だったのだけれど、 たくさん書いてると多少偏見もなおって考えを改めたりした部分があるのでまとめる…