proposition: Lemma setX2_P x y z: inc z (product2 x y) <-> [/\ fgraph z, domain z = C2 , inc (Vg z C0) x & inc (Vg z C1) y].
proof: Proof. split. move /(setXf_P) => [fa fb fc]; split => //. move: (fc _ inc_C0_C2); aww. move: (fc _ inc_C1_C2); aww. move => [pa pb pc pd]; apply/(setXf_P). by split ; aw;trivial => i ind; try_lvariant ind. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)