equal
deleted
inserted
replaced
612 proof (induct n arbitrary: l r) |
612 proof (induct n arbitrary: l r) |
613 case 0 |
613 case 0 |
614 have "fcard_raw l = 0" by fact |
614 have "fcard_raw l = 0" by fact |
615 then have "\<forall>x. \<not> memb x l" using memb_card_not_0[of _ l] by auto |
615 then have "\<forall>x. \<not> memb x l" using memb_card_not_0[of _ l] by auto |
616 then have z: "l = []" using no_memb_nil by auto |
616 then have z: "l = []" using no_memb_nil by auto |
617 then have "r = []" sorry |
617 then have "r = []" using `l \<approx> r` by simp |
618 then show ?case using z list_eq2_refl by simp |
618 then show ?case using z list_eq2_refl by simp |
619 next |
619 next |
620 case (Suc m) |
620 case (Suc m) |
621 have b: "l \<approx> r" by fact |
621 have b: "l \<approx> r" by fact |
622 have d: "fcard_raw l = Suc m" by fact |
622 have d: "fcard_raw l = Suc m" by fact |