proposition: Lemma Exercise6_33e n: inc n c -> sub (Vf X n) M.
proof: Proof. move: Exercise6_33d => [[fx ix] sx tx]. rewrite /E6_33_M => nc t tw; apply /setUb_P; aw;ex_tac;rewrite LgV//. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)