datatype aaa = A | B lemma "(a ~= A) --> (a = B)"
Как доказать эту основную лемму? Я относительно новичок в Изабель, и проблема сбивает с толку.
С помощью кейс-анализа на:
by (cases a, auto)