[STATEMENT]
lemma vars_Const [simp]: "vars (Const c) = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vars (Const c) = {}
[PROOF STEP]
unfolding vars_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Union> (keys ` keys (mapping_of (Const c))) = {}
[PROOF STEP]
by transfer' (auto simp: keys_Const\<^sub>0)