proposition: Lemma prl_ne1_res2: (exists2 j, inc j (psI S) & forall i, inc i (psI S) -> gle (psr S) i j) -> forall i, inc i (psI S) -> surjection (prl_can_fun S i).
proof: Proof. move => [j jI jge]. move => i iI; move: (jge _ iI) => h; apply:(prl_ne1_surj_rec h). move:(prl_can_fun_fp jI) => [fa sa ta]; split=> //; rewrite sa ta {i iI h}. move => y ys. set x := Lg (psI S) (fun i => Vf (Vg (psf S) (J i j)) y). have xp: inc x (projective_limit S). rewrite /x; apply/prl_limitP; aw; split; fprops. move => i iI; rewrite LgV//; move: (ps_function_f (jge _ iI)); aw => - [fb sb tb];Wtac. move => i k leik. move: (arg1_sr leik) (arg2_sr leik). rewrite ps_substrate_r => iI kI; rewrite ! LgV//. by rewrite (prl_prop3 leik (jge _ kI) ys). exists x => //;rewrite prl_proj_ev // /x; rewrite LgV//. by rewrite (ps_identity_f jI) idV//. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)