changeset 9664 | 4cae97480a6d |
parent 9594 | 42d11e0a7a8b |
child 9757 | 1024a2d80ac0 |
9663:e4d58f1be05b | 9664:4cae97480a6d |
---|---|
239 fix l ls assume IH: "?P ls" |
239 fix l ls assume IH: "?P ls" |
240 |
240 |
241 { |
241 { |
242 fix b |
242 fix b |
243 have "?Q (l#ls) b" |
243 have "?Q (l#ls) b" |
244 proof (cases b) |
244 proof (cases (open) b) |
245 case Nil |
245 case Nil |
246 thus ?thesis by (auto dest: sup_loc_length) |
246 thus ?thesis by (auto dest: sup_loc_length) |
247 next |
247 next |
248 case Cons |
248 case Cons |
249 show ?thesis |
249 show ?thesis |