proposition: Lemma Exercise6_33d3 n: inc n c -> nonempty (Vf X n).
proof: Proof. move: Exercise6_33d => [[fx ix] <- tx] ns. by move: (Vf_target fx ns); rewrite tx => /setC1_P [_] /nonemptyP. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)