equal
deleted
inserted
replaced
139 apply(drule meta_mp) |
139 apply(drule meta_mp) |
140 apply(simp add: fresh_at_base) |
140 apply(simp add: fresh_at_base) |
141 apply(simp add: insert_fset_left_comm) |
141 apply(simp add: insert_fset_left_comm) |
142 done |
142 done |
143 |
143 |
144 lemma weakening_version4: |
|
145 fixes \<Gamma>::"(name \<times> ty) fset" |
|
146 assumes a: "\<Gamma> 2\<turnstile> t : T" |
|
147 and b: "(x, T') |\<notin>| \<Gamma>" |
|
148 shows "{|(x, T')|} |\<union>| \<Gamma> 2\<turnstile> t : T" |
|
149 using a b |
|
150 apply(induct \<Gamma> t T arbitrary: x) |
|
151 apply(auto)[2] |
|
152 apply(rule t2_Lam) |
|
153 oops |
|
154 |
144 |
155 end |
145 end |
156 |
146 |
157 |
147 |
158 |
148 |