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