140 

   140 

   141 lemma Rep_perm_ext:

   141 lemma Rep_perm_ext:

   142   "Rep_perm p1 = Rep_perm p2 \<Longrightarrow> p1 = p2"

   142   "Rep_perm p1 = Rep_perm p2 \<Longrightarrow> p1 = p2"

   143   by (simp add: fun_eq_iff Rep_perm_inject [symmetric])

   143   by (simp add: fun_eq_iff Rep_perm_inject [symmetric])

   144 

   144 

   145 

   146 

   146 subsection {* Permutations form a group *}

   147 subsection {* Permutations form a group *}

   147 

   148 

   148 instantiation perm :: group_add

   149 instantiation perm :: group_add

   149 begin

   150 begin