proposition: Lemma prl_proj_ax S i: inc i (psI S) -> lf_axiom (fun x => Vg x i) (projective_limit S) (Vg (psE S) i).
proof: Proof. by move => ide x /prl_limitP[_ _ p3 _]; apply: p3. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)