[STATEMENT]
lemma fmdrop_idle': "x \<notin> fmdom' B \<Longrightarrow> fmdrop x B = B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<notin> fmdom' B \<Longrightarrow> fmdrop x B = B
[PROOF STEP]
by transfer' (auto simp: map_drop_def map_filter_def)