proposition: Lemma prl_map_ax S u F : prl_map_compat S u F -> lf_axiom (prl_map_val S u ) F (projective_limit S).
proof: Proof. move => [cp1 cp2 cp3 cp4] y yF. rewrite cp2 in cp3. rewrite /prl_map_val;apply/prl_limitP;aw;split; fprops. move => i iI. move: (cp3 i iI) => [fui sui tui]. by rewrite !LgV// - tui; apply: (Vf_target fui); rewrite sui. move => i j lij; rewrite /prl_map_val /=. move:(prl_prop0 lij) => [isr jsr]. move: (cp3 _ jsr) => [fuj suj tuj]. have ysr: inc y (source (Vg u j)) by rewrite suj. have cop: Vg (psf S) (J i j) \coP Vg u j. move:(ps_function_f lij) => [ff sf tf]. by split => //; rewrite sf tuj pr2_pair. rewrite !LgV//; move/(f_equal (fun z => (Vf z y))):(cp4 _ _ lij). by rewrite compfV. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)