proposition: Lemma prl_ne2_nonempty_bis: (forall i, inc i (psI S) -> prl_ne1_condii' i) -> prl_ne2_res_a -> nonempty (projective_limit S).
proof: Proof. move => ha hb. case:(emptyset_dichot (psI S)) => ine. rewrite (prl_trivial ine); apply: set1_ne. move:ine => [i iI]; move: (hb i iI) => hc. suff: nonempty (Imf (prl_can_fun S i)). move: (prl_can_fun_fp iI) => [ff sf tf]. move => [x /(Imf_P ff) [u]]; rewrite sf => uE _; ex_tac. rewrite hc;apply:(prl_ne2_res4b iI (ha _ iI)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)