[STATEMENT]
lemma Some_in_opt [iff]:
  "(Some x \<in> opt A) = (x\<in>A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Some x \<in> opt A) = (x \<in> A)
[PROOF STEP]
apply (unfold opt_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Some x \<in> insert None {x. \<exists>y\<in>A. x = Some y}) = (x \<in> A)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done