equal
deleted
inserted
replaced
601 proof (induct n arbitrary: l r) |
601 proof (induct n arbitrary: l r) |
602 case 0 |
602 case 0 |
603 have "fcard_raw l = 0" by fact |
603 have "fcard_raw l = 0" by fact |
604 then have "\<forall>x. \<not> memb x l" using memb_card_not_0[of _ l] by auto |
604 then have "\<forall>x. \<not> memb x l" using memb_card_not_0[of _ l] by auto |
605 then have z: "l = []" using no_memb_nil by auto |
605 then have z: "l = []" using no_memb_nil by auto |
606 then have "r = []" sorry |
606 then have "r = []" using `l \<approx> r` by simp |
607 then show ?case using z list_eq2_refl by simp |
607 then show ?case using z list_eq2_refl by simp |
608 next |
608 next |
609 case (Suc m) |
609 case (Suc m) |
610 have b: "l \<approx> r" by fact |
610 have b: "l \<approx> r" by fact |
611 have d: "fcard_raw l = Suc m" by fact |
611 have d: "fcard_raw l = Suc m" by fact |