equal
deleted
inserted
replaced
328 prefer 2 |
328 prefer 2 |
329 apply clarify |
329 apply clarify |
330 apply (rename_tac m n) |
330 apply (rename_tac m n) |
331 apply (case_tac "m=n") |
331 apply (case_tac "m=n") |
332 apply simp |
332 apply simp |
333 apply (fast intro!: equals0I [to_pred bot_empty_eq] dest: not_sym) |
333 apply (fast intro!: equals0I [to_pred bot_empty_eq pred_equals_eq] dest: not_sym) |
334 apply clarify |
334 apply clarify |
335 apply (rename_tac n) |
335 apply (rename_tac n) |
336 apply (induct_tac n) |
336 apply (induct_tac n) |
337 apply (simp add: lesssub_def cong: conj_cong) |
337 apply (simp add: lesssub_def cong: conj_cong) |
338 apply (rename_tac k) |
338 apply (rename_tac k) |