equal
deleted
inserted
replaced
285 apply (rule b2) |
285 apply (rule b2) |
286 done |
286 done |
287 next |
287 next |
288 case (3 name lam pi a) |
288 case (3 name lam pi a) |
289 have b: "\<And>(pi::name prm) a. P a (pi \<bullet> lam)" by fact |
289 have b: "\<And>(pi::name prm) a. P a (pi \<bullet> lam)" by fact |
290 obtain c::name where fr: "c\<sharp>(a, pi\<bullet>name, pi\<bullet>lam)" sorry |
290 obtain c::name where fr: "c\<sharp>(a, pi\<bullet>name, pi\<bullet>lam)" |
|
291 apply(rule exists_fresh[of "(a, pi\<bullet>name, pi\<bullet>lam)"]) |
|
292 apply(simp_all add: fs_name1) |
|
293 done |
291 from b fr have p: "P a (Lam c (([(c, pi\<bullet>name)]@pi)\<bullet>lam))" |
294 from b fr have p: "P a (Lam c (([(c, pi\<bullet>name)]@pi)\<bullet>lam))" |
292 apply - |
295 apply - |
293 apply(rule a3) |
296 apply(rule a3) |
294 apply(blast) |
297 apply(blast) |
295 apply(simp) |
298 apply(simp) |