proposition: Lemma compfV g f x: g \coP f -> inc x (source f) -> Vf (g \co f) x = Vf g (Vf f x).
proof: Proof. rewrite /Vf => cgf xs; rewrite compf_graph=>//. apply: composef_ev; rewrite domain_fg //; fct_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)