equal
deleted
inserted
replaced
126 and fc: "atom x \<sharp> \<Gamma>" |
126 and fc: "atom x \<sharp> \<Gamma>" |
127 obtains T1 T2 where "T = T1 \<rightarrow> T2" "(x, T1) # \<Gamma> \<turnstile> t : T2" |
127 obtains T1 T2 where "T = T1 \<rightarrow> T2" "(x, T1) # \<Gamma> \<turnstile> t : T2" |
128 using ty fc |
128 using ty fc |
129 apply(cases) |
129 apply(cases) |
130 using [[simproc del: alpha_lst]] |
130 using [[simproc del: alpha_lst]] |
131 apply(auto simp add: lam.eq_iff lam.distinct ty.eq_iff) |
|
132 apply(auto simp add: Abs1_eq_iff) |
131 apply(auto simp add: Abs1_eq_iff) |
133 apply(rotate_tac 3) |
132 apply(rotate_tac 4) |
134 apply(drule_tac p="(x \<leftrightarrow> xa)" in permute_boolI) |
133 apply(drule_tac p="(x \<leftrightarrow> xa)" in permute_boolI) |
135 apply(perm_simp) |
134 apply(perm_simp) |
136 apply(auto simp add: flip_fresh_fresh ty_fresh) |
135 apply(auto simp add: flip_fresh_fresh ty_fresh) |
137 done |
136 done |
138 |
137 |