usefulness of `in_set1`

[affeldt-aist]

analysis/classical/classical_sets.v

Line 2199 in e2db34a

Lemma in_set1 [T : finType] (x y : T) : (x \in [set y]) = (x \in [set y]%SET).

As observed by @t6s in the conversion of PR #1827 , in_set1 is not used in master :

#1827 (comment)

Also, in_set1 might be more appropriate for this lemma:

Lemma in_set1_eq {T : eqType} (a : T) (x : T) : x \in [set a] = (x == a).

What about replacing the current in_set1 by in_set1_eq? @CohenCyril

FYI: @Yosuke-Ito-345