[STATEMENT]
lemma subst_typ_rename_tvar_preserves_eq:
  "(y, S) \<notin> tvsT T \<Longrightarrow> (y, S) \<notin> tvsT \<tau> \<Longrightarrow>
    subst_typ [((x, S), Tv y S)] T = subst_typ [((x, S), Tv y S)] \<tau> \<Longrightarrow> T=\<tau>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(y, S) \<notin> tvsT T; (y, S) \<notin> tvsT \<tau>; subst_typ [((x, S), Tv y S)] T = subst_typ [((x, S), Tv y S)] \<tau>\<rbrakk> \<Longrightarrow> T = \<tau>
[PROOF STEP]
proof (induction T arbitrary: \<tau>)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x1 x2 \<tau>. \<lbrakk>\<And>x2a \<tau>. \<lbrakk>x2a \<in> set x2; (y, S) \<notin> tvsT x2a; (y, S) \<notin> tvsT \<tau>; subst_typ [((x, S), Tv y S)] x2a = subst_typ [((x, S), Tv y S)] \<tau>\<rbrakk> \<Longrightarrow> x2a = \<tau>; (y, S) \<notin> tvsT (Ty x1 x2); (y, S) \<notin> tvsT \<tau>; subst_typ [((x, S), Tv y S)] (Ty x1 x2) = subst_typ [((x, S), Tv y S)] \<tau>\<rbrakk> \<Longrightarrow> Ty x1 x2 = \<tau>
 2. \<And>x1 x2 \<tau>. \<lbrakk>(y, S) \<notin> tvsT (Tv x1 x2); (y, S) \<notin> tvsT \<tau>; subst_typ [((x, S), Tv y S)] (Tv x1 x2) = subst_typ [((x, S), Tv y S)] \<tau>\<rbrakk> \<Longrightarrow> Tv x1 x2 = \<tau>
[PROOF STEP]
case (Ty n Ts)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?x2a \<in> set Ts; (y, S) \<notin> tvsT ?x2a; (y, S) \<notin> tvsT ?\<tau>; subst_typ [((x, S), Tv y S)] ?x2a = subst_typ [((x, S), Tv y S)] ?\<tau>\<rbrakk> \<Longrightarrow> ?x2a = ?\<tau>
(y, S) \<notin> tvsT (Ty n Ts)
(y, S) \<notin> tvsT \<tau>
subst_typ [((x, S), Tv y S)] (Ty n Ts) = subst_typ [((x, S), Tv y S)] \<tau>

goal (2 subgoals):
 1. \<And>x1 x2 \<tau>. \<lbrakk>\<And>x2a \<tau>. \<lbrakk>x2a \<in> set x2; (y, S) \<notin> tvsT x2a; (y, S) \<notin> tvsT \<tau>; subst_typ [((x, S), Tv y S)] x2a = subst_typ [((x, S), Tv y S)] \<tau>\<rbrakk> \<Longrightarrow> x2a = \<tau>; (y, S) \<notin> tvsT (Ty x1 x2); (y, S) \<notin> tvsT \<tau>; subst_typ [((x, S), Tv y S)] (Ty x1 x2) = subst_typ [((x, S), Tv y S)] \<tau>\<rbrakk> \<Longrightarrow> Ty x1 x2 = \<tau>
 2. \<And>x1 x2 \<tau>. \<lbrakk>(y, S) \<notin> tvsT (Tv x1 x2); (y, S) \<notin> tvsT \<tau>; subst_typ [((x, S), Tv y S)] (Tv x1 x2) = subst_typ [((x, S), Tv y S)] \<tau>\<rbrakk> \<Longrightarrow> Tv x1 x2 = \<tau>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?x2a \<in> set Ts; (y, S) \<notin> tvsT ?x2a; (y, S) \<notin> tvsT ?\<tau>; subst_typ [((x, S), Tv y S)] ?x2a = subst_typ [((x, S), Tv y S)] ?\<tau>\<rbrakk> \<Longrightarrow> ?x2a = ?\<tau>
(y, S) \<notin> tvsT (Ty n Ts)
(y, S) \<notin> tvsT \<tau>
subst_typ [((x, S), Tv y S)] (Ty n Ts) = subst_typ [((x, S), Tv y S)] \<tau>
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x2a \<in> set Ts; (y, S) \<notin> tvsT ?x2a; (y, S) \<notin> tvsT ?\<tau>; subst_typ [((x, S), Tv y S)] ?x2a = subst_typ [((x, S), Tv y S)] ?\<tau>\<rbrakk> \<Longrightarrow> ?x2a = ?\<tau>
(y, S) \<notin> tvsT (Ty n Ts)
(y, S) \<notin> tvsT \<tau>
subst_typ [((x, S), Tv y S)] (Ty n Ts) = subst_typ [((x, S), Tv y S)] \<tau>

goal (1 subgoal):
 1. Ty n Ts = \<tau>
[PROOF STEP]
proof (induction \<tau>)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x1 x2. \<lbrakk>\<And>x2a. \<lbrakk>x2a \<in> set x2; \<And>x2a \<tau>. \<lbrakk>x2a \<in> set Ts; (y, S) \<notin> tvsT x2a; (y, S) \<notin> tvsT \<tau>; subst_typ [((x, S), Tv y S)] x2a = subst_typ [((x, S), Tv y S)] \<tau>\<rbrakk> \<Longrightarrow> x2a = \<tau>; (y, S) \<notin> tvsT (Ty n Ts); (y, S) \<notin> tvsT x2a; subst_typ [((x, S), Tv y S)] (Ty n Ts) = subst_typ [((x, S), Tv y S)] x2a\<rbrakk> \<Longrightarrow> Ty n Ts = x2a; \<And>x2a \<tau>. \<lbrakk>x2a \<in> set Ts; (y, S) \<notin> tvsT x2a; (y, S) \<notin> tvsT \<tau>; subst_typ [((x, S), Tv y S)] x2a = subst_typ [((x, S), Tv y S)] \<tau>\<rbrakk> \<Longrightarrow> x2a = \<tau>; (y, S) \<notin> tvsT (Ty n Ts); (y, S) \<notin> tvsT (Ty x1 x2); subst_typ [((x, S), Tv y S)] (Ty n Ts) = subst_typ [((x, S), Tv y S)] (Ty x1 x2)\<rbrakk> \<Longrightarrow> Ty n Ts = Ty x1 x2
 2. \<And>x1 x2. \<lbrakk>\<And>x2a \<tau>. \<lbrakk>x2a \<in> set Ts; (y, S) \<notin> tvsT x2a; (y, S) \<notin> tvsT \<tau>; subst_typ [((x, S), Tv y S)] x2a = subst_typ [((x, S), Tv y S)] \<tau>\<rbrakk> \<Longrightarrow> x2a = \<tau>; (y, S) \<notin> tvsT (Ty n Ts); (y, S) \<notin> tvsT (Tv x1 x2); subst_typ [((x, S), Tv y S)] (Ty n Ts) = subst_typ [((x, S), Tv y S)] (Tv x1 x2)\<rbrakk> \<Longrightarrow> Ty n Ts = Tv x1 x2
[PROOF STEP]
case (Ty n Ts)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?x2a \<in> set Ts; \<And>x2a \<tau>. \<lbrakk>x2a \<in> set Ts__; (y, S) \<notin> tvsT x2a; (y, S) \<notin> tvsT \<tau>; subst_typ [((x, S), Tv y S)] x2a = subst_typ [((x, S), Tv y S)] \<tau>\<rbrakk> \<Longrightarrow> x2a = \<tau>; (y, S) \<notin> tvsT (Ty n__ Ts__); (y, S) \<notin> tvsT ?x2a; subst_typ [((x, S), Tv y S)] (Ty n__ Ts__) = subst_typ [((x, S), Tv y S)] ?x2a\<rbrakk> \<Longrightarrow> Ty n__ Ts__ = ?x2a
\<lbrakk>?x2a \<in> set Ts__; (y, S) \<notin> tvsT ?x2a; (y, S) \<notin> tvsT ?\<tau>; subst_typ [((x, S), Tv y S)] ?x2a = subst_typ [((x, S), Tv y S)] ?\<tau>\<rbrakk> \<Longrightarrow> ?x2a = ?\<tau>
(y, S) \<notin> tvsT (Ty n__ Ts__)
(y, S) \<notin> tvsT (Ty n Ts)
subst_typ [((x, S), Tv y S)] (Ty n__ Ts__) = subst_typ [((x, S), Tv y S)] (Ty n Ts)

goal (2 subgoals):
 1. \<And>x1 x2. \<lbrakk>\<And>x2a. \<lbrakk>x2a \<in> set x2; \<And>x2a \<tau>. \<lbrakk>x2a \<in> set Ts__; (y, S) \<notin> tvsT x2a; (y, S) \<notin> tvsT \<tau>; subst_typ [((x, S), Tv y S)] x2a = subst_typ [((x, S), Tv y S)] \<tau>\<rbrakk> \<Longrightarrow> x2a = \<tau>; (y, S) \<notin> tvsT (Ty n__ Ts__); (y, S) \<notin> tvsT x2a; subst_typ [((x, S), Tv y S)] (Ty n__ Ts__) = subst_typ [((x, S), Tv y S)] x2a\<rbrakk> \<Longrightarrow> Ty n__ Ts__ = x2a; \<And>x2a \<tau>. \<lbrakk>x2a \<in> set Ts__; (y, S) \<notin> tvsT x2a; (y, S) \<notin> tvsT \<tau>; subst_typ [((x, S), Tv y S)] x2a = subst_typ [((x, S), Tv y S)] \<tau>\<rbrakk> \<Longrightarrow> x2a = \<tau>; (y, S) \<notin> tvsT (Ty n__ Ts__); (y, S) \<notin> tvsT (Ty x1 x2); subst_typ [((x, S), Tv y S)] (Ty n__ Ts__) = subst_typ [((x, S), Tv y S)] (Ty x1 x2)\<rbrakk> \<Longrightarrow> Ty n__ Ts__ = Ty x1 x2
 2. \<And>x1 x2. \<lbrakk>\<And>x2a \<tau>. \<lbrakk>x2a \<in> set Ts__; (y, S) \<notin> tvsT x2a; (y, S) \<notin> tvsT \<tau>; subst_typ [((x, S), Tv y S)] x2a = subst_typ [((x, S), Tv y S)] \<tau>\<rbrakk> \<Longrightarrow> x2a = \<tau>; (y, S) \<notin> tvsT (Ty n__ Ts__); (y, S) \<notin> tvsT (Tv x1 x2); subst_typ [((x, S), Tv y S)] (Ty n__ Ts__) = subst_typ [((x, S), Tv y S)] (Tv x1 x2)\<rbrakk> \<Longrightarrow> Ty n__ Ts__ = Tv x1 x2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?x2a \<in> set Ts; \<And>x2a \<tau>. \<lbrakk>x2a \<in> set Ts__; (y, S) \<notin> tvsT x2a; (y, S) \<notin> tvsT \<tau>; subst_typ [((x, S), Tv y S)] x2a = subst_typ [((x, S), Tv y S)] \<tau>\<rbrakk> \<Longrightarrow> x2a = \<tau>; (y, S) \<notin> tvsT (Ty n__ Ts__); (y, S) \<notin> tvsT ?x2a; subst_typ [((x, S), Tv y S)] (Ty n__ Ts__) = subst_typ [((x, S), Tv y S)] ?x2a\<rbrakk> \<Longrightarrow> Ty n__ Ts__ = ?x2a
\<lbrakk>?x2a \<in> set Ts__; (y, S) \<notin> tvsT ?x2a; (y, S) \<notin> tvsT ?\<tau>; subst_typ [((x, S), Tv y S)] ?x2a = subst_typ [((x, S), Tv y S)] ?\<tau>\<rbrakk> \<Longrightarrow> ?x2a = ?\<tau>
(y, S) \<notin> tvsT (Ty n__ Ts__)
(y, S) \<notin> tvsT (Ty n Ts)
subst_typ [((x, S), Tv y S)] (Ty n__ Ts__) = subst_typ [((x, S), Tv y S)] (Ty n Ts)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x2a \<in> set Ts; \<And>x2a \<tau>. \<lbrakk>x2a \<in> set Ts__; (y, S) \<notin> tvsT x2a; (y, S) \<notin> tvsT \<tau>; subst_typ [((x, S), Tv y S)] x2a = subst_typ [((x, S), Tv y S)] \<tau>\<rbrakk> \<Longrightarrow> x2a = \<tau>; (y, S) \<notin> tvsT (Ty n__ Ts__); (y, S) \<notin> tvsT ?x2a; subst_typ [((x, S), Tv y S)] (Ty n__ Ts__) = subst_typ [((x, S), Tv y S)] ?x2a\<rbrakk> \<Longrightarrow> Ty n__ Ts__ = ?x2a
\<lbrakk>?x2a \<in> set Ts__; (y, S) \<notin> tvsT ?x2a; (y, S) \<notin> tvsT ?\<tau>; subst_typ [((x, S), Tv y S)] ?x2a = subst_typ [((x, S), Tv y S)] ?\<tau>\<rbrakk> \<Longrightarrow> ?x2a = ?\<tau>
(y, S) \<notin> tvsT (Ty n__ Ts__)
(y, S) \<notin> tvsT (Ty n Ts)
subst_typ [((x, S), Tv y S)] (Ty n__ Ts__) = subst_typ [((x, S), Tv y S)] (Ty n Ts)

goal (1 subgoal):
 1. Ty n__ Ts__ = Ty n Ts
[PROOF STEP]
by simp (smt list.inj_map_strong)
[PROOF STATE]
proof (state)
this:
Ty n__ Ts__ = Ty n Ts

goal (1 subgoal):
 1. \<And>x1 x2. \<lbrakk>\<And>x2a \<tau>. \<lbrakk>x2a \<in> set Ts__; (y, S) \<notin> tvsT x2a; (y, S) \<notin> tvsT \<tau>; subst_typ [((x, S), Tv y S)] x2a = subst_typ [((x, S), Tv y S)] \<tau>\<rbrakk> \<Longrightarrow> x2a = \<tau>; (y, S) \<notin> tvsT (Ty n__ Ts__); (y, S) \<notin> tvsT (Tv x1 x2); subst_typ [((x, S), Tv y S)] (Ty n__ Ts__) = subst_typ [((x, S), Tv y S)] (Tv x1 x2)\<rbrakk> \<Longrightarrow> Ty n__ Ts__ = Tv x1 x2
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x1 x2. \<lbrakk>\<And>x2a \<tau>. \<lbrakk>x2a \<in> set Ts; (y, S) \<notin> tvsT x2a; (y, S) \<notin> tvsT \<tau>; subst_typ [((x, S), Tv y S)] x2a = subst_typ [((x, S), Tv y S)] \<tau>\<rbrakk> \<Longrightarrow> x2a = \<tau>; (y, S) \<notin> tvsT (Ty n Ts); (y, S) \<notin> tvsT (Tv x1 x2); subst_typ [((x, S), Tv y S)] (Ty n Ts) = subst_typ [((x, S), Tv y S)] (Tv x1 x2)\<rbrakk> \<Longrightarrow> Ty n Ts = Tv x1 x2
[PROOF STEP]
case (Tv n S)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?x2a \<in> set Ts; (y, S) \<notin> tvsT ?x2a; (y, S) \<notin> tvsT ?\<tau>; subst_typ [((x, S), Tv y S)] ?x2a = subst_typ [((x, S), Tv y S)] ?\<tau>\<rbrakk> \<Longrightarrow> ?x2a = ?\<tau>
(y, S) \<notin> tvsT (Ty n__ Ts)
(y, S) \<notin> tvsT (Tv n S)
subst_typ [((x, S), Tv y S)] (Ty n__ Ts) = subst_typ [((x, S), Tv y S)] (Tv n S)

goal (1 subgoal):
 1. \<And>x1 x2. \<lbrakk>\<And>x2a \<tau>. \<lbrakk>x2a \<in> set Ts; (y, S) \<notin> tvsT x2a; (y, S) \<notin> tvsT \<tau>; subst_typ [((x, S), Tv y S)] x2a = subst_typ [((x, S), Tv y S)] \<tau>\<rbrakk> \<Longrightarrow> x2a = \<tau>; (y, S) \<notin> tvsT (Ty n__ Ts); (y, S) \<notin> tvsT (Tv x1 x2); subst_typ [((x, S), Tv y S)] (Ty n__ Ts) = subst_typ [((x, S), Tv y S)] (Tv x1 x2)\<rbrakk> \<Longrightarrow> Ty n__ Ts = Tv x1 x2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?x2a \<in> set Ts; (y, S) \<notin> tvsT ?x2a; (y, S) \<notin> tvsT ?\<tau>; subst_typ [((x, S), Tv y S)] ?x2a = subst_typ [((x, S), Tv y S)] ?\<tau>\<rbrakk> \<Longrightarrow> ?x2a = ?\<tau>
(y, S) \<notin> tvsT (Ty n__ Ts)
(y, S) \<notin> tvsT (Tv n S)
subst_typ [((x, S), Tv y S)] (Ty n__ Ts) = subst_typ [((x, S), Tv y S)] (Tv n S)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x2a \<in> set Ts; (y, S) \<notin> tvsT ?x2a; (y, S) \<notin> tvsT ?\<tau>; subst_typ [((x, S), Tv y S)] ?x2a = subst_typ [((x, S), Tv y S)] ?\<tau>\<rbrakk> \<Longrightarrow> ?x2a = ?\<tau>
(y, S) \<notin> tvsT (Ty n__ Ts)
(y, S) \<notin> tvsT (Tv n S)
subst_typ [((x, S), Tv y S)] (Ty n__ Ts) = subst_typ [((x, S), Tv y S)] (Tv n S)

goal (1 subgoal):
 1. Ty n__ Ts = Tv n S
[PROOF STEP]
by (auto split: if_splits)
[PROOF STATE]
proof (state)
this:
Ty n__ Ts = Tv n S

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Ty n Ts = \<tau>

goal (1 subgoal):
 1. \<And>x1 x2 \<tau>. \<lbrakk>(y, S) \<notin> tvsT (Tv x1 x2); (y, S) \<notin> tvsT \<tau>; subst_typ [((x, S), Tv y S)] (Tv x1 x2) = subst_typ [((x, S), Tv y S)] \<tau>\<rbrakk> \<Longrightarrow> Tv x1 x2 = \<tau>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x1 x2 \<tau>. \<lbrakk>(y, S) \<notin> tvsT (Tv x1 x2); (y, S) \<notin> tvsT \<tau>; subst_typ [((x, S), Tv y S)] (Tv x1 x2) = subst_typ [((x, S), Tv y S)] \<tau>\<rbrakk> \<Longrightarrow> Tv x1 x2 = \<tau>
[PROOF STEP]
case (Tv n S)
[PROOF STATE]
proof (state)
this:
(y, S) \<notin> tvsT (Tv n S)
(y, S) \<notin> tvsT \<tau>
subst_typ [((x, S), Tv y S)] (Tv n S) = subst_typ [((x, S), Tv y S)] \<tau>

goal (1 subgoal):
 1. \<And>x1 x2 \<tau>. \<lbrakk>(y, S) \<notin> tvsT (Tv x1 x2); (y, S) \<notin> tvsT \<tau>; subst_typ [((x, S), Tv y S)] (Tv x1 x2) = subst_typ [((x, S), Tv y S)] \<tau>\<rbrakk> \<Longrightarrow> Tv x1 x2 = \<tau>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(y, S) \<notin> tvsT (Tv n S)
(y, S) \<notin> tvsT \<tau>
subst_typ [((x, S), Tv y S)] (Tv n S) = subst_typ [((x, S), Tv y S)] \<tau>
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(y, S) \<notin> tvsT (Tv n S)
(y, S) \<notin> tvsT \<tau>
subst_typ [((x, S), Tv y S)] (Tv n S) = subst_typ [((x, S), Tv y S)] \<tau>

goal (1 subgoal):
 1. Tv n S = \<tau>
[PROOF STEP]
by (induction \<tau>) (auto split: if_splits)
[PROOF STATE]
proof (state)
this:
Tv n S = \<tau>

goal:
No subgoals!
[PROOF STEP]
qed