proposition: Lemma setX1_canon_V x a i: inc i x -> Vf (product1_canon x a) i = cst_graph (singleton a) i.
proof: Proof. by move=> iw; rewrite LfV //; apply: setX1_canon_axiom. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)