proposition: Lemma projective_map_ev S u F x i: prl_map_compat S u F -> inc x F -> inc i (psI S) -> Vg (Vf (projective_map S u F) x) i = Vf (Vg u i) x.
proof: Proof. move => /prl_map_ax ax xF iI. rewrite /projective_map /prl_map_val LfV// LgV//. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)