equal
deleted
inserted
replaced
209 done |
209 done |
210 |
210 |
211 lemma t3_elim: "\<lbrakk>\<Gamma> \<turnstile> Lam [a].t : \<sigma>;a\<sharp>\<Gamma>\<rbrakk>\<Longrightarrow> \<exists>\<tau> \<tau>'. \<sigma>=\<tau>\<rightarrow>\<tau>' \<and> ((a,\<tau>)#\<Gamma>) \<turnstile> t : \<tau>'" |
211 lemma t3_elim: "\<lbrakk>\<Gamma> \<turnstile> Lam [a].t : \<sigma>;a\<sharp>\<Gamma>\<rbrakk>\<Longrightarrow> \<exists>\<tau> \<tau>'. \<sigma>=\<tau>\<rightarrow>\<tau>' \<and> ((a,\<tau>)#\<Gamma>) \<turnstile> t : \<tau>'" |
212 apply(ind_cases2 "\<Gamma> \<turnstile> Lam [a].t : \<sigma>") |
212 apply(ind_cases2 "\<Gamma> \<turnstile> Lam [a].t : \<sigma>") |
213 apply(auto simp add: lam.distinct lam.inject alpha) |
213 apply(auto simp add: lam.distinct lam.inject alpha) |
214 apply(drule_tac pi="[(a,aa)]::name prm" in typing_eqvt) |
214 apply(drule_tac pi="[(a,aa)]::name prm" in typing.eqvt) |
215 apply(simp) |
215 apply(simp) |
216 apply(subgoal_tac "([(a,aa)]::name prm)\<bullet>\<Gamma> = \<Gamma>")(*A*) |
216 apply(subgoal_tac "([(a,aa)]::name prm)\<bullet>\<Gamma> = \<Gamma>")(*A*) |
217 apply(force simp add: calc_atm) |
217 apply(force simp add: calc_atm) |
218 (*A*) |
218 (*A*) |
219 apply(force intro!: perm_fresh_fresh) |
219 apply(force intro!: perm_fresh_fresh) |