[STATEMENT]
lemma fun_upd2_comm:
assumes "a' = a \<and> b' = b \<longrightarrow> c' = c"
shows "fun_upd2 (fun_upd2 f a b c) a' b' c' = fun_upd2 (fun_upd2 f a' b' c') a b c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fun_upd2 (fun_upd2 f a b c) a' b' c' = fun_upd2 (fun_upd2 f a' b' c') a b c
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
a' = a \<and> b' = b \<longrightarrow> c' = c

goal (1 subgoal):
 1. fun_upd2 (fun_upd2 f a b c) a' b' c' = fun_upd2 (fun_upd2 f a' b' c') a b c
[PROOF STEP]
unfolding fun_upd2_def
[PROOF STATE]
proof (prove)
using this:
a' = a \<and> b' = b \<longrightarrow> c' = c

goal (1 subgoal):
 1. (\<lambda>a'a b'a. if a' = a'a \<and> b' = b'a then c' else if a = a'a \<and> b = b'a then c else f a'a b'a) = (\<lambda>a'a b'a. if a = a'a \<and> b = b'a then c else if a' = a'a \<and> b' = b'a then c' else f a'a b'a)
[PROOF STEP]
by (intro ext) auto