やっと証明に入りました。 2.3 An Introductory Proof 証明の大まかな流れを追ってみます。Main Goal.リストにrevを二回適用すると元に戻ることを証明します。 theorem rev_rev [simp]: "rev (rev xs) = xs" theoremは新しい定理"rev (rev xs) = xs"を証明し…