proposition: Lemma prl_ne1_allE_ne: prl_ne1_some_nonempty -> forall i, inc i (psI S) -> nonempty(Vg (psE S) i).
proof: Proof. move => [i iI [x xEi]] j jI. rewrite - ps_substrate_r in iI jI. move:(rdr iI jI) => [k [le1 le2]]. move: (ps_function_f le1)(ps_function_f le2) => [ff1 sf1 tf1] [ff2 sf2 tf2]. have xt: inc x (target (Vg (psf S) (J i k))) by rewrite tf1; aw. move:(proj2 (sjf le1) _ xt); rewrite sf1; aw; move => [y ya _]. move:(Vf_target ff2); rewrite sf2 tf2;aw => h; move: (h _ ya) => yb; ex_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)