481 lemma fset_to_set_simps[simp]:

   481 lemma fset_to_set_simps[simp]:

   482   "fset_to_set {||} = ({} :: 'a set)"

   482   "fset_to_set {||} = ({} :: 'a set)"

   483   "fset_to_set (finsert (h :: 'a) t) = insert h (fset_to_set t)"

   483   "fset_to_set (finsert (h :: 'a) t) = insert h (fset_to_set t)"

   484   by (lifting set.simps)

   484   by (lifting set.simps)

   485 

   485 

   488 lemma in_fset_to_set:

   486 lemma in_fset_to_set:

   489   "x \<in> fset_to_set S \<equiv> x |\<in>| S"

   487   "x \<in> fset_to_set S \<equiv> x |\<in>| S"

   490   by (lifting memb_def[symmetric])

   488   by (lifting memb_def[symmetric])

   491 

   489 

   492 lemma none_fin_fempty:

   490 lemma none_fin_fempty: