proposition: Lemma setU1K a B : a \notin B -> (a |: B) :\ a = B.
proof: Proof. by move/negPf=> nBa; apply/setP=> x /[!inE]; case: eqP => // ->. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)