Remove duplicate unique perm instance

PR #8387 already gave this
leanprover-community · Jul 25, 2021 · ac1353b · ac1353b
1 parent 36b5ca1
commit ac1353b
Showing 1 changed file with 0 additions and 3 deletions.
diff --git a/src/data/equiv/basic.lean b/src/data/equiv/basic.lean
@@ -179,9 +179,6 @@ equiv.equiv_subsingleton_cod
 lemma perm.subsingleton_eq_refl [subsingleton α] (e : perm α) :
   e = equiv.refl α := subsingleton.elim _ _
 
-instance equiv.unique_of_subsingleton {α : Type*} [subsingleton α] : unique (α ≃ α) :=
-unique_of_subsingleton (equiv.refl α)
-
 /-- Transfer `decidable_eq` across an equivalence. -/
 protected def decidable_eq (e : α ≃ β) [decidable_eq β] : decidable_eq α :=
 e.injective.decidable_eq