2 imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "../QuotMain" "Abs" "../QuotProd"

     2 imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "../QuotMain" "Abs" "../QuotProd"

     3 begin

     3 begin

     4 

     4 

     5 

     5 

     6 (* lemmas that should be in Nominal \<dots>\<dots>must be cleaned *)

     6 (* lemmas that should be in Nominal \<dots>\<dots>must be cleaned *)

     7 lemma supp_finite_set:

     8 lemma supp_finite_set:

     8   fixes S::"atom set"

     9   fixes S::"atom set"

     9   assumes "finite S"

    10   assumes "finite S"

    10   shows "supp S = S"

    11   shows "supp S = S"

    11   apply(rule finite_supp_unique)

    12   apply(rule finite_supp_unique)