proposition: Lemma setX_lS x x' y: nonempty y -> sub (x \times y) (x' \times y) -> sub x x'.
proof: Proof. by move=> [t ty] s z zx; move: (s _ (setXp_i zx ty)); case/setXp_P. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)