proposition: Lemma select_pr1 (p : property) E: (exists2 x, inc x E & p x) -> (singl_val2 (inc ^~ E) p) -> p (select p E).
proof: Proof. move => ha hb; exact: (proj1 (select_pr ha hb)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)