proposition: Lemma setX_set1 f: (allf f singletonp) -> singletonp (productb f).
proof: Proof. move=> als; apply/singletonP; split. by apply: setXb_ne => i idf; move /singletonP: (als _ idf) => []. move=> a b ap bp; apply: (setXb_exten ap bp)=> i id. move /singletonP: (als _ id) => [ne eq]; apply: eq. by move/setXb_P: ap => [_ _ ]; apply. by move/setXb_P: bp => [_ _ ]; apply. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)