1.1 --- a/src/HOL/BNF/Countable_Type.thy	Mon Jul 15 11:29:19 2013 +0200
     1.2 +++ b/src/HOL/BNF/Countable_Type.thy	Mon Jul 15 14:23:51 2013 +0200
     1.3 @@ -92,10 +92,6 @@
     1.4  "countable (rcset C)"
     1.5  using Rep_cset by simp
     1.6  
     1.7 -lemma rcset_inj[simp]:
     1.8 -"rcset C = rcset D \<longleftrightarrow> C = D"
     1.9 -by (metis acset_rcset)
    1.10 -
    1.11  lemma rcset_surj:
    1.12  assumes "countable A"
    1.13  shows "\<exists> C. rcset C = A"