[STATEMENT]
lemma in_keysD: "k \<in> keys m \<Longrightarrow> \<exists>v. lookup m k = Some v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k \<in> keys m \<Longrightarrow> \<exists>v. lookup m k = Some v
[PROOF STEP]
by transfer (fact domD)