proposition: Lemma pri_V f i x: inc i (domain f) -> inc x (productb f) -> Vf (pr_i f i) x = Vg x i.
proof: Proof. by rewrite/pr_i=> id xp; rewrite LfV // ; apply: pri_axiom. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)