proposition: Lemma prl_proj_ev S i x: inc i (psI S) -> inc x (projective_limit S) -> Vf (prl_can_fun S i) x = Vg x i.
proof: Proof. by move => ha hb;rewrite /prl_can_fun LfV//; apply:prl_proj_ax. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)