proposition: Lemma prl_map_prop S u F : prl_map_compat S u F -> prl_map_property S u F (projective_map S u F).
proof: Proof. move => hb. move:(prl_map_ax hb) => hc. set g := (projective_map S u F). have fg: function g by apply:lf_function. have sg: source g = F by rewrite /g/projective_map; aw. have tg: target g = (projective_limit S) by rewrite /g/projective_map; aw. have gp:inc g (functions F (projective_limit S)) by apply/functionsP. move: hb => [hb1 hb2 hb3 hb4]. split => // i idu. move: (hb3 _ idu) => [fui sui tui]. have ide:inc i (psI S) by rewrite - hb2. move: (prl_can_fun_fp ide) => [fp sp tp]. have cop:prl_can_fun S i \coP g by split => //; ue. apply:function_exten;[ done | by apply: compf_f | by aw; rewrite sg | | ]. by aw; rewrite tp. rewrite sui; move => j jsu /=. have jsg: inc j (source g) by rewrite sg. have aux: inc (Vf g j) (projective_limit S) by Wtac. rewrite compfV //prl_proj_ev // projective_map_ev //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)