proposition: Lemma set1_pr x X: inc x X -> alls X (eq^~ x) -> X = singleton x.
proof: Proof. move=> xX zy; set_extens t; first by move => ty;apply/set1_P;apply: zy. by move /set1_P ->. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)