[STATEMENT]
lemma undefg_equiv: "(\<alpha>\<noteq>undefg) = (\<exists>g. \<alpha>=Agame g)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<alpha> \<noteq> undefg) = (\<exists>g. \<alpha> = Agame g)
[PROOF STEP]
by simp