proposition: Lemma prl_ne2_prop_trivial: (exists2 i, inc i (psI S) & Vg (psE S) i = emptyset) -> prl_ne2_res_a.
proof: Proof. move => [j jI Ee] i iI. move: (prl_can_fun_fp iI) => [ff sf tf]. set_extens t. move/(Imf_P ff); rewrite sf; move => [u /prl_limitP [_ _ ok _] _]. by move:(ok _ jI); rewrite Ee => /in_set0. move:(iI) (jI); rewrite - ps_substrate_r => ir jr. move:(rdr ir jr) => [k [leik lejk]]. move:(prl_prop4 lejk) => [fjk sjk tjk]; rewrite Ee in tjk. move: (empty_function_p2 fjk tjk); rewrite sjk => se. move:(prl_prop4 leik) => [fik sik tik]. move/ prl_ne2_intP: leik => kZ ti;move:(setIf_hi ti kZ) => /(Imf_P fik). by rewrite sik se; move => [u /in_set0]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)