278 lemma "fcard X = Suc n \<Longrightarrow> (\<exists>a S. a \<notin>f S & X = finsert a S)"

   278 lemma "fcard X = Suc n \<Longrightarrow> (\<exists>a S. a \<notin>f S & X = finsert a S)"

   279 (*by (lifting card_raw_suc)*)

   279 (*by (lifting card_raw_suc)*)

   280 sorry

   280 sorry

   281 

   281 

   282 thm card_raw_cons_gt_0

   282 thm card_raw_cons_gt_0

   284 thm not_nil_equiv_cons

   284 thm not_nil_equiv_cons

   285 thm delete_raw.simps

   285 thm delete_raw.simps

   286 (*thm mem_delete_raw*)

   286 (*thm mem_delete_raw*)

   287 thm card_raw_delete_raw

   287 thm card_raw_delete_raw

   288 thm cons_delete_raw

   288 thm cons_delete_raw