[STATEMENT]
lemma (in LCD) foldD_insert:
  assumes "finite A" "x \<notin> A" "x \<in> B" "e \<in> D" "A \<subseteq> B"
  shows "foldD D f e (insert x A) = f x (foldD D f e A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. foldD D (\<cdot>) e (insert x A) = x \<cdot> foldD D (\<cdot>) e A
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. foldD D (\<cdot>) e (insert x A) = x \<cdot> foldD D (\<cdot>) e A
[PROOF STEP]
have "(THE v. \<exists>y. (A, y) \<in> foldSetD D (\<cdot>) e \<and> v = x \<cdot> y) = x \<cdot> (THE y. (A, y) \<in> foldSetD D (\<cdot>) e)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (THE v. \<exists>y. (A, y) \<in> foldSetD D (\<cdot>) e \<and> v = x \<cdot> y) = x \<cdot> (THE y. (A, y) \<in> foldSetD D (\<cdot>) e)
[PROOF STEP]
by (rule the_equality) (use assms foldD_def foldD_equality foldD_def finite_imp_foldSetD in \<open>metis+\<close>)
[PROOF STATE]
proof (state)
this:
(THE v. \<exists>y. (A, y) \<in> foldSetD D (\<cdot>) e \<and> v = x \<cdot> y) = x \<cdot> (THE y. (A, y) \<in> foldSetD D (\<cdot>) e)

goal (1 subgoal):
 1. foldD D (\<cdot>) e (insert x A) = x \<cdot> foldD D (\<cdot>) e A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(THE v. \<exists>y. (A, y) \<in> foldSetD D (\<cdot>) e \<and> v = x \<cdot> y) = x \<cdot> (THE y. (A, y) \<in> foldSetD D (\<cdot>) e)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(THE v. \<exists>y. (A, y) \<in> foldSetD D (\<cdot>) e \<and> v = x \<cdot> y) = x \<cdot> (THE y. (A, y) \<in> foldSetD D (\<cdot>) e)

goal (1 subgoal):
 1. foldD D (\<cdot>) e (insert x A) = x \<cdot> foldD D (\<cdot>) e A
[PROOF STEP]
unfolding foldD_def
[PROOF STATE]
proof (prove)
using this:
(THE v. \<exists>y. (A, y) \<in> foldSetD D (\<cdot>) e \<and> v = x \<cdot> y) = x \<cdot> (THE y. (A, y) \<in> foldSetD D (\<cdot>) e)

goal (1 subgoal):
 1. (THE xa. (insert x A, xa) \<in> foldSetD D (\<cdot>) e) = x \<cdot> (THE x. (A, x) \<in> foldSetD D (\<cdot>) e)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(THE v. \<exists>y. (A, y) \<in> foldSetD D (\<cdot>) e \<and> v = x \<cdot> y) = x \<cdot> (THE y. (A, y) \<in> foldSetD D (\<cdot>) e)
finite A
x \<notin> A
x \<in> B
e \<in> D
A \<subseteq> B

goal (1 subgoal):
 1. (THE xa. (insert x A, xa) \<in> foldSetD D (\<cdot>) e) = x \<cdot> (THE x. (A, x) \<in> foldSetD D (\<cdot>) e)
[PROOF STEP]
by (simp add: foldD_insert_aux)
[PROOF STATE]
proof (state)
this:
foldD D (\<cdot>) e (insert x A) = x \<cdot> foldD D (\<cdot>) e A

goal:
No subgoals!
[PROOF STEP]
qed