proposition: Lemma set1Ul x A b : x \in A -> x \in A :|: [set b].
proof: Proof. by move=> Ax; rewrite !inE Ax. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)