proposition: Lemma prl_can_fun_fp S i: inc i (psI S) -> function_prop (prl_can_fun S i) (projective_limit S) (Vg (psE S) i).
proof: Proof. move => ide; rewrite /prl_can_fun. saw; apply:lf_function; exact:prl_proj_ax. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)