proposition: Lemma setX_domain x y: nonempty y -> domain (x \times y) = x.
proof: Proof. move=> [z zy]; set_extens t. by case/funI_P => u /setX_P [_ xx _] ->. move=> tx; apply/funI_P;exists (J t z); aw; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)