datatype aaa = A | B lemma "(a ~= A) --> (a = B)"
How to prove this basic lemma? I'm relatively new to Isabelle, and the problem is confusing.
Via case-analysis on a:
by (cases a, auto)