proposition: Lemma eq_set1P (T : finType) (A : {set T}) (x : T) : reflect (x \in A /\ {in A, all_equal_to x}) (A == [set x]).
proof: Proof. apply: (iffP eqP) => [->|]; first by rewrite !in_set1; by split => // y /set1P. case => H1 H2. apply/setP => y. apply/idP/set1P;[exact: H2| by move ->]. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone)