equal
deleted
inserted
replaced
192 thm eqvts_raw |
192 thm eqvts_raw |
193 |
193 |
194 lemma |
194 lemma |
195 assumes a: "alpha_lam_raw' t1 t2" |
195 assumes a: "alpha_lam_raw' t1 t2" |
196 shows "alpha_lam_raw' (p \<bullet> t1) (p \<bullet> t2)" |
196 shows "alpha_lam_raw' (p \<bullet> t1) (p \<bullet> t2)" |
|
197 using a |
|
198 apply(induct) |
|
199 apply(perm_simp) |
|
200 apply(rule a1) |
|
201 apply(simp) |
|
202 apply(perm_simp) |
|
203 apply(rule a2) |
|
204 apply(simp) |
|
205 apply(simp) |
|
206 apply(perm_simp) |
|
207 apply(rule a3) |
|
208 apply(unfold alpha_gen) |
197 oops |
209 oops |
198 |
210 |
199 lemma |
211 lemma |
200 assumes a: "alpha_lam_raw' t1 t2" |
212 assumes a: "alpha_lam_raw' t1 t2" |
201 shows "alpha_lam_raw' (p \<bullet> t1) (p \<bullet> t2)" |
213 shows "alpha_lam_raw' (p \<bullet> t1) (p \<bullet> t2)" |