proposition: Lemma in_set pA x : x \in finset pA = pA x.
proof: Proof. by rewrite [@finset]unlock unlock [x \in _]ffunE. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)