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