[STATEMENT]
lemma not_Err_eq: "(x \<noteq> Err) = (\<exists>a. x = OK a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<noteq> Err) = (\<exists>a. x = OK a)
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<noteq> Err) = (\<exists>a. x = OK a)
[PROOF STEP]
by (cases x) auto