前回のうまくいかない elim の続きで，Coq'Art 15 章に載っている方針による別証明について。なぜそっちはうまくいくのか。ちなみにここに書くことが Coq'Art にきちんと解説されていたかどうかは覚えていませんが，こういうことを細かく解説したものを読ん…