[STATEMENT]
lemma psubst_eq_subst:
  assumes "\<phi> \<in> fmla" "x \<in> var" and "t \<in> trm"
  shows "psubst \<phi> [(t,x)] = subst \<phi> t x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. psubst \<phi> [(t, x)] = subst \<phi> t x
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. psubst \<phi> [(t, x)] = subst \<phi> t x
[PROOF STEP]
have "psubst \<phi> [(t,x)] = rawpsubst \<phi> [(t,x)]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. psubst \<phi> [(t, x)] = rawpsubst \<phi> [(t, x)]
[PROOF STEP]
apply(rule psubst_eq_rawpsubst)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<phi> \<in> fmla
 2. snd ` set [(t, x)] \<subseteq> var
 3. fst ` set [(t, x)] \<subseteq> trm
 4. distinct (map snd [(t, x)])
 5. \<And>i j. \<lbrakk>i < j; j < length [(t, x)]\<rbrakk> \<Longrightarrow> snd ([(t, x)] ! j) \<notin> FvarsT (fst ([(t, x)] ! i))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<phi> \<in> fmla
x \<in> var
t \<in> trm

goal (5 subgoals):
 1. \<phi> \<in> fmla
 2. snd ` set [(t, x)] \<subseteq> var
 3. fst ` set [(t, x)] \<subseteq> trm
 4. distinct (map snd [(t, x)])
 5. \<And>i j. \<lbrakk>i < j; j < length [(t, x)]\<rbrakk> \<Longrightarrow> snd ([(t, x)] ! j) \<notin> FvarsT (fst ([(t, x)] ! i))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
psubst \<phi> [(t, x)] = rawpsubst \<phi> [(t, x)]

goal (1 subgoal):
 1. psubst \<phi> [(t, x)] = subst \<phi> t x
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
psubst \<phi> [(t, x)] = rawpsubst \<phi> [(t, x)]

goal (1 subgoal):
 1. psubst \<phi> [(t, x)] = subst \<phi> t x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
psubst \<phi> [(t, x)] = subst \<phi> t x

goal:
No subgoals!
[PROOF STEP]
qed