proposition: Lemma setU1_mem (T : finType) x (A : {set T}) : x \in A -> x |: A = A.
proof: Proof. move => H. apply/setP => y. rewrite !inE. case: (boolP (y == x)) => // /eqP ->. by rewrite H. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone)