[STATEMENT]
lemma fresh_Some:
  shows "a \<sharp> Some x \<longleftrightarrow> a \<sharp> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<sharp> Some x = a \<sharp> x
[PROOF STEP]
by (simp add: fresh_def supp_Some)