今日の証明 Netを覗いて見ると。A→AのCoqでの証明例があり試してみた。 Coqは定理証明支援系の一つです。 Coq証明②で演繹定理を適用して、(intros.) A → Aを A ⇒ Aに置き換えている。Ａ⇒Ａは、「ＡはＡであると結論付ける」と読む。 Aをリンゴ(apple)とすれ…