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

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

     3 begin

     3 begin

     4 

     4 

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

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

     6 lemma in_permute_iff:

     6 lemma in_permute_iff:

   320 lemma abs_eq:

   320 lemma abs_eq:

   321   shows "(Abs as x) = (Abs bs y) \<longleftrightarrow> (\<exists>pi. supp x - as = supp y - bs \<and> (supp x - as) \<sharp>* pi \<and> pi \<bullet> x = y)"

   321   shows "(Abs as x) = (Abs bs y) \<longleftrightarrow> (\<exists>pi. supp x - as = supp y - bs \<and> (supp x - as) \<sharp>* pi \<and> pi \<bullet> x = y)"

   322 apply(lifting alpha_abs.simps(1))

   322 apply(lifting alpha_abs.simps(1))

   323 done

   323 done

   324 

   324