[STATEMENT]
lemma relevant_vars_subl:
  assumes "\<forall>x \<in> vars\<^sub>l l. \<sigma>\<^sub>1 x = \<sigma>\<^sub>2 x "
  shows "l \<cdot>\<^sub>l \<sigma>\<^sub>1 = l \<cdot>\<^sub>l \<sigma>\<^sub>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l \<cdot>\<^sub>l \<sigma>\<^sub>1 = l \<cdot>\<^sub>l \<sigma>\<^sub>2
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>vars\<^sub>l l. \<sigma>\<^sub>1 x = \<sigma>\<^sub>2 x

goal (1 subgoal):
 1. l \<cdot>\<^sub>l \<sigma>\<^sub>1 = l \<cdot>\<^sub>l \<sigma>\<^sub>2
[PROOF STEP]
proof (induction l)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x1 x2. \<forall>x\<in>vars\<^sub>l (Pos x1 x2). \<sigma>\<^sub>1 x = \<sigma>\<^sub>2 x \<Longrightarrow> Pos x1 x2 \<cdot>\<^sub>l \<sigma>\<^sub>1 = Pos x1 x2 \<cdot>\<^sub>l \<sigma>\<^sub>2
 2. \<And>x1 x2. \<forall>x\<in>vars\<^sub>l (Neg x1 x2). \<sigma>\<^sub>1 x = \<sigma>\<^sub>2 x \<Longrightarrow> Neg x1 x2 \<cdot>\<^sub>l \<sigma>\<^sub>1 = Neg x1 x2 \<cdot>\<^sub>l \<sigma>\<^sub>2
[PROOF STEP]
case (Pos p ts)
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>vars\<^sub>l (Pos p ts). \<sigma>\<^sub>1 x = \<sigma>\<^sub>2 x

goal (2 subgoals):
 1. \<And>x1 x2. \<forall>x\<in>vars\<^sub>l (Pos x1 x2). \<sigma>\<^sub>1 x = \<sigma>\<^sub>2 x \<Longrightarrow> Pos x1 x2 \<cdot>\<^sub>l \<sigma>\<^sub>1 = Pos x1 x2 \<cdot>\<^sub>l \<sigma>\<^sub>2
 2. \<And>x1 x2. \<forall>x\<in>vars\<^sub>l (Neg x1 x2). \<sigma>\<^sub>1 x = \<sigma>\<^sub>2 x \<Longrightarrow> Neg x1 x2 \<cdot>\<^sub>l \<sigma>\<^sub>1 = Neg x1 x2 \<cdot>\<^sub>l \<sigma>\<^sub>2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>x\<in>vars\<^sub>l (Pos p ts). \<sigma>\<^sub>1 x = \<sigma>\<^sub>2 x
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>vars\<^sub>l (Pos p ts). \<sigma>\<^sub>1 x = \<sigma>\<^sub>2 x

goal (1 subgoal):
 1. Pos p ts \<cdot>\<^sub>l \<sigma>\<^sub>1 = Pos p ts \<cdot>\<^sub>l \<sigma>\<^sub>2
[PROOF STEP]
using relevant_vars_subts
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>vars\<^sub>l (Pos p ts). \<sigma>\<^sub>1 x = \<sigma>\<^sub>2 x
\<forall>x\<in>vars\<^sub>t\<^sub>s ?ts. ?\<sigma>\<^sub>1 x = ?\<sigma>\<^sub>2 x \<Longrightarrow> ?ts \<cdot>\<^sub>t\<^sub>s ?\<sigma>\<^sub>1 = ?ts \<cdot>\<^sub>t\<^sub>s ?\<sigma>\<^sub>2

goal (1 subgoal):
 1. Pos p ts \<cdot>\<^sub>l \<sigma>\<^sub>1 = Pos p ts \<cdot>\<^sub>l \<sigma>\<^sub>2
[PROOF STEP]
unfolding vars\<^sub>l_def
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>vars\<^sub>t\<^sub>s (get_terms (Pos p ts)). \<sigma>\<^sub>1 x = \<sigma>\<^sub>2 x
\<forall>x\<in>vars\<^sub>t\<^sub>s ?ts. ?\<sigma>\<^sub>1 x = ?\<sigma>\<^sub>2 x \<Longrightarrow> ?ts \<cdot>\<^sub>t\<^sub>s ?\<sigma>\<^sub>1 = ?ts \<cdot>\<^sub>t\<^sub>s ?\<sigma>\<^sub>2

goal (1 subgoal):
 1. Pos p ts \<cdot>\<^sub>l \<sigma>\<^sub>1 = Pos p ts \<cdot>\<^sub>l \<sigma>\<^sub>2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Pos p ts \<cdot>\<^sub>l \<sigma>\<^sub>1 = Pos p ts \<cdot>\<^sub>l \<sigma>\<^sub>2

goal (1 subgoal):
 1. \<And>x1 x2. \<forall>x\<in>vars\<^sub>l (Neg x1 x2). \<sigma>\<^sub>1 x = \<sigma>\<^sub>2 x \<Longrightarrow> Neg x1 x2 \<cdot>\<^sub>l \<sigma>\<^sub>1 = Neg x1 x2 \<cdot>\<^sub>l \<sigma>\<^sub>2
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x1 x2. \<forall>x\<in>vars\<^sub>l (Neg x1 x2). \<sigma>\<^sub>1 x = \<sigma>\<^sub>2 x \<Longrightarrow> Neg x1 x2 \<cdot>\<^sub>l \<sigma>\<^sub>1 = Neg x1 x2 \<cdot>\<^sub>l \<sigma>\<^sub>2
[PROOF STEP]
case (Neg p ts)
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>vars\<^sub>l (Neg p ts). \<sigma>\<^sub>1 x = \<sigma>\<^sub>2 x

goal (1 subgoal):
 1. \<And>x1 x2. \<forall>x\<in>vars\<^sub>l (Neg x1 x2). \<sigma>\<^sub>1 x = \<sigma>\<^sub>2 x \<Longrightarrow> Neg x1 x2 \<cdot>\<^sub>l \<sigma>\<^sub>1 = Neg x1 x2 \<cdot>\<^sub>l \<sigma>\<^sub>2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>x\<in>vars\<^sub>l (Neg p ts). \<sigma>\<^sub>1 x = \<sigma>\<^sub>2 x
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>vars\<^sub>l (Neg p ts). \<sigma>\<^sub>1 x = \<sigma>\<^sub>2 x

goal (1 subgoal):
 1. Neg p ts \<cdot>\<^sub>l \<sigma>\<^sub>1 = Neg p ts \<cdot>\<^sub>l \<sigma>\<^sub>2
[PROOF STEP]
using relevant_vars_subts
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>vars\<^sub>l (Neg p ts). \<sigma>\<^sub>1 x = \<sigma>\<^sub>2 x
\<forall>x\<in>vars\<^sub>t\<^sub>s ?ts. ?\<sigma>\<^sub>1 x = ?\<sigma>\<^sub>2 x \<Longrightarrow> ?ts \<cdot>\<^sub>t\<^sub>s ?\<sigma>\<^sub>1 = ?ts \<cdot>\<^sub>t\<^sub>s ?\<sigma>\<^sub>2

goal (1 subgoal):
 1. Neg p ts \<cdot>\<^sub>l \<sigma>\<^sub>1 = Neg p ts \<cdot>\<^sub>l \<sigma>\<^sub>2
[PROOF STEP]
unfolding vars\<^sub>l_def
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>vars\<^sub>t\<^sub>s (get_terms (Neg p ts)). \<sigma>\<^sub>1 x = \<sigma>\<^sub>2 x
\<forall>x\<in>vars\<^sub>t\<^sub>s ?ts. ?\<sigma>\<^sub>1 x = ?\<sigma>\<^sub>2 x \<Longrightarrow> ?ts \<cdot>\<^sub>t\<^sub>s ?\<sigma>\<^sub>1 = ?ts \<cdot>\<^sub>t\<^sub>s ?\<sigma>\<^sub>2

goal (1 subgoal):
 1. Neg p ts \<cdot>\<^sub>l \<sigma>\<^sub>1 = Neg p ts \<cdot>\<^sub>l \<sigma>\<^sub>2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Neg p ts \<cdot>\<^sub>l \<sigma>\<^sub>1 = Neg p ts \<cdot>\<^sub>l \<sigma>\<^sub>2

goal:
No subgoals!
[PROOF STEP]
qed