[STATEMENT]
lemma fv_Cons[simp]: "fv (x # xs) = fv x \<union> fv xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fv (x # xs) = fv x \<union> fv xs
[PROOF STEP]
by (auto simp add: fv_def supp_Cons)