[STATEMENT]
lemma keysFor_insert_Key [simp]: "keysFor (insert (Key K) H) = keysFor H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. keysFor (insert (Key K) H) = keysFor H
[PROOF STEP]
by (unfold keysFor_def, auto)