proposition: Lemma char_fun_V A B x : inc x B -> Vf (char_fun A B) x = (varianti A \1c \0c x).
proof: Proof. move=> xB; rewrite /char_fun LfV //; apply: char_fun_axioms. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)