[STATEMENT]
lemma map_upd_eqD1:
  assumes "m(a\<mapsto>x) = n(a\<mapsto>y)"
  shows "x = y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = y
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x = y
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
m(a \<mapsto> x) = n(a \<mapsto> y)
[PROOF STEP]
have "(m(a\<mapsto>x)) a = (n(a\<mapsto>y)) a"
[PROOF STATE]
proof (prove)
using this:
m(a \<mapsto> x) = n(a \<mapsto> y)

goal (1 subgoal):
 1. (m(a \<mapsto> x)) a = (n(a \<mapsto> y)) a
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(m(a \<mapsto> x)) a = (n(a \<mapsto> y)) a

goal (1 subgoal):
 1. x = y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(m(a \<mapsto> x)) a = (n(a \<mapsto> y)) a
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(m(a \<mapsto> x)) a = (n(a \<mapsto> y)) a

goal (1 subgoal):
 1. x = y
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x = y

goal:
No subgoals!
[PROOF STEP]
qed