[STATEMENT]
lemma subst_all_num[simp]:
  assumes "\<phi> \<in> fmla" "x \<in> var" "y \<in> var" "n \<in> num"
  shows "x \<noteq> y \<Longrightarrow> subst (all x \<phi>) n y = all x (subst \<phi> n y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<noteq> y \<Longrightarrow> subst (all x \<phi>) n y = all x (subst \<phi> n y)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<phi> \<in> fmla
x \<in> var
y \<in> var
n \<in> num

goal (1 subgoal):
 1. x \<noteq> y \<Longrightarrow> subst (all x \<phi>) n y = all x (subst \<phi> n y)
[PROOF STEP]
by simp