[STATEMENT]
lemma eq_subst_scheme_list_eq_free:
  "\<lbrakk> $S1 (A::type_scheme list) = $S2 A;  n:(free_tv A) \<rbrakk> \<Longrightarrow> S1 n = S2 n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>$ S1 A = $ S2 A; n \<in> free_tv A\<rbrakk> \<Longrightarrow> S1 n = S2 n
[PROOF STEP]
proof (induct A)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>$ S1 [] = $ S2 []; n \<in> free_tv []\<rbrakk> \<Longrightarrow> S1 n = S2 n
 2. \<And>a A. \<lbrakk>\<lbrakk>$ S1 A = $ S2 A; n \<in> free_tv A\<rbrakk> \<Longrightarrow> S1 n = S2 n; $ S1 (a # A) = $ S2 (a # A); n \<in> free_tv (a # A)\<rbrakk> \<Longrightarrow> S1 n = S2 n
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
$ S1 [] = $ S2 []
n \<in> free_tv []

goal (2 subgoals):
 1. \<lbrakk>$ S1 [] = $ S2 []; n \<in> free_tv []\<rbrakk> \<Longrightarrow> S1 n = S2 n
 2. \<And>a A. \<lbrakk>\<lbrakk>$ S1 A = $ S2 A; n \<in> free_tv A\<rbrakk> \<Longrightarrow> S1 n = S2 n; $ S1 (a # A) = $ S2 (a # A); n \<in> free_tv (a # A)\<rbrakk> \<Longrightarrow> S1 n = S2 n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
$ S1 [] = $ S2 []
n \<in> free_tv []
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
$ S1 [] = $ S2 []
n \<in> free_tv []

goal (1 subgoal):
 1. S1 n = S2 n
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
S1 n = S2 n

goal (1 subgoal):
 1. \<And>a A. \<lbrakk>\<lbrakk>$ S1 A = $ S2 A; n \<in> free_tv A\<rbrakk> \<Longrightarrow> S1 n = S2 n; $ S1 (a # A) = $ S2 (a # A); n \<in> free_tv (a # A)\<rbrakk> \<Longrightarrow> S1 n = S2 n
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a A. \<lbrakk>\<lbrakk>$ S1 A = $ S2 A; n \<in> free_tv A\<rbrakk> \<Longrightarrow> S1 n = S2 n; $ S1 (a # A) = $ S2 (a # A); n \<in> free_tv (a # A)\<rbrakk> \<Longrightarrow> S1 n = S2 n
[PROOF STEP]
case Cons
[PROOF STATE]
proof (state)
this:
\<lbrakk>$ S1 A_ = $ S2 A_; n \<in> free_tv A_\<rbrakk> \<Longrightarrow> S1 n = S2 n
$ S1 (a_ # A_) = $ S2 (a_ # A_)
n \<in> free_tv (a_ # A_)

goal (1 subgoal):
 1. \<And>a A. \<lbrakk>\<lbrakk>$ S1 A = $ S2 A; n \<in> free_tv A\<rbrakk> \<Longrightarrow> S1 n = S2 n; $ S1 (a # A) = $ S2 (a # A); n \<in> free_tv (a # A)\<rbrakk> \<Longrightarrow> S1 n = S2 n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>$ S1 A_ = $ S2 A_; n \<in> free_tv A_\<rbrakk> \<Longrightarrow> S1 n = S2 n
$ S1 (a_ # A_) = $ S2 (a_ # A_)
n \<in> free_tv (a_ # A_)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>$ S1 A_ = $ S2 A_; n \<in> free_tv A_\<rbrakk> \<Longrightarrow> S1 n = S2 n
$ S1 (a_ # A_) = $ S2 (a_ # A_)
n \<in> free_tv (a_ # A_)

goal (1 subgoal):
 1. S1 n = S2 n
[PROOF STEP]
by (fastforce intro: eq_subst_type_scheme_eq_free)
[PROOF STATE]
proof (state)
this:
S1 n = S2 n

goal:
No subgoals!
[PROOF STEP]
qed