[STATEMENT]
lemma fresh_var_eqE[elim_format]: "fresh_var e = x \<Longrightarrow> x \<notin>  fv e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fresh_var e = x \<Longrightarrow> x \<notin> fv e
[PROOF STEP]
by (metis fresh_var_not_free)