proposition: Lemma setX2_canon_V x y z: inc z (x \times y) -> Vf (product2_canon x y) z = variantLc (P z) (Q z).
proof: Proof. move => zp;rewrite LfV //; by apply: setX2_canon_axiom. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)