783   and   "Abs_lst [c] x = Abs_lst [c] y \<longleftrightarrow> x = y"

   783   and   "Abs_lst [c] x = Abs_lst [c] y \<longleftrightarrow> x = y"

   784 unfolding Abs_eq_iff2 alphas

   784 unfolding Abs_eq_iff2 alphas

   785 apply(simp_all add: supp_perm_singleton fresh_star_def fresh_zero_perm)

   785 apply(simp_all add: supp_perm_singleton fresh_star_def fresh_zero_perm)

   786 apply(blast)+

   786 apply(blast)+

   787 done

   787 done

   789 

   788 

   790 lemma Abs1_eq_iff:

   789 lemma Abs1_eq_iff:

   791   fixes x::"'a::fs"

   790   fixes x::"'a::fs"

   792   assumes "sort_of a = sort_of b"

   791   assumes "sort_of a = sort_of b"

   793   and     "sort_of c = sort_of d"

   792   and     "sort_of c = sort_of d"