1308 lemma supp_insert_fset [simp]:

  1308 lemma supp_insert_fset [simp]:

  1309   fixes x::"'a::fs"

  1309   fixes x::"'a::fs"

  1310   and   S::"'a fset"

  1310   and   S::"'a fset"

  1311   shows "supp (insert_fset x S) = supp x \<union> supp S"

  1311   shows "supp (insert_fset x S) = supp x \<union> supp S"

  1312   apply(subst supp_fset[symmetric])

  1312   apply(subst supp_fset[symmetric])

  1314   done

  1314   done

  1315 

  1315 

  1316 lemma fset_finite_supp:

  1316 lemma fset_finite_supp:

  1317   fixes S::"('a::fs) fset"

  1317   fixes S::"('a::fs) fset"

  1318   shows "finite (supp S)"

  1318   shows "finite (supp S)"