proposition: Lemma char_fun_V_a A B x: sub A B -> inc x A -> Vf (char_fun A B) x = \1c.
proof: Proof. move=> AB xA; rewrite (char_fun_V A (AB _ xA)). by apply: varianti_in. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)