proposition: Lemma prl_singleton_prop S k (f := Lf (Vg ^~ k) (projective_limit S) (Vg (psE S) k)): inc k (psI S) -> (forall i, inc i (psI S) -> gle (psr S) i k) -> bijection_prop f (projective_limit S) (Vg (psE S) k).
proof: Proof. move => kI kg. move: (prl_proj_ax kI) (prl_can_fun_fp kI) => ax ff. rewrite /f;split; aw; trivial; apply:lf_bijective => //. move => x y /prl_limitP[g xd xv xw] /prl_limitP[yg yd yv yw] sv. apply:fgraph_exten => //; rewrite xd => // i iI. by rewrite (xw _ _ (kg _ iI)) (yw _ _ (kg _ iI)) sv. move => y yk. pose x := Lg (psI S) (fun i => Vf (Vg (psf S) (J i k)) y). have yvv: y = Vg x k by rewrite /x LgV// (ps_identity_f kI) idV. exists x => //; rewrite/x;apply/prl_limitP; aw; split;fprops. move => i iI; rewrite LgV//. move:(ps_function_f (kg _ iI)); aw => - [fij sik tik]; Wtac. move => i j lij; move: (prl_prop0 lij) => [iI jI]; rewrite ! LgV//. by rewrite(prl_prop3 lij (kg _ jI) yk). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)