[STATEMENT]
lemma map_val_raw_cong:
  assumes "\<And>k v. (k, v) \<in> set (fst xs) \<Longrightarrow> f k v = g k v"
  shows "map_val_raw f xs = map_val_raw g xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_val_raw f xs = map_val_raw g xs
[PROOF STEP]
proof (rule map_raw_cong)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>kv. kv \<in> set (fst xs) \<Longrightarrow> (case kv of (k, v) \<Rightarrow> (k, f k v)) = (case kv of (k, v) \<Rightarrow> (k, g k v))
[PROOF STEP]
fix kv
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>kv. kv \<in> set (fst xs) \<Longrightarrow> (case kv of (k, v) \<Rightarrow> (k, f k v)) = (case kv of (k, v) \<Rightarrow> (k, g k v))
[PROOF STEP]
assume "kv \<in> set (fst xs)"
[PROOF STATE]
proof (state)
this:
kv \<in> set (fst xs)

goal (1 subgoal):
 1. \<And>kv. kv \<in> set (fst xs) \<Longrightarrow> (case kv of (k, v) \<Rightarrow> (k, f k v)) = (case kv of (k, v) \<Rightarrow> (k, g k v))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
kv \<in> set (fst xs)

goal (1 subgoal):
 1. \<And>kv. kv \<in> set (fst xs) \<Longrightarrow> (case kv of (k, v) \<Rightarrow> (k, f k v)) = (case kv of (k, v) \<Rightarrow> (k, g k v))
[PROOF STEP]
obtain k v where "kv = (k, v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>k v. kv = (k, v) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
kv = (k, v)

goal (1 subgoal):
 1. \<And>kv. kv \<in> set (fst xs) \<Longrightarrow> (case kv of (k, v) \<Rightarrow> (k, f k v)) = (case kv of (k, v) \<Rightarrow> (k, g k v))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
kv \<in> set (fst xs)
kv = (k, v)
[PROOF STEP]
show "(case kv of (k, v) \<Rightarrow> (k, f k v)) = (case kv of (k, v) \<Rightarrow> (k, g k v))"
[PROOF STATE]
proof (prove)
using this:
kv \<in> set (fst xs)
kv = (k, v)

goal (1 subgoal):
 1. (case kv of (k, v) \<Rightarrow> (k, f k v)) = (case kv of (k, v) \<Rightarrow> (k, g k v))
[PROOF STEP]
by (simp add: assms)
[PROOF STATE]
proof (state)
this:
(case kv of (k, v) \<Rightarrow> (k, f k v)) = (case kv of (k, v) \<Rightarrow> (k, g k v))

goal:
No subgoals!
[PROOF STEP]
qed