proposition: Lemma prl_proj_image_prop1 S i j: gle (psr S) i j -> sub (prl_proj_image S i) (Imf (Vg (psf S) (J i j))).
proof: Proof. move => lij. move:(prl_prop0 lij) => [iI jI]. move: (prl_can_fun_fp iI) => [fi si ti]. move:(ps_function_f lij) => [fij sij tij]. move => t /(Imf_P fi) [u us ->]. have ax := (prl_proj_ax iI). rewrite si in us. rewrite /prl_can_fun; aw; apply/(Imf_P fij);rewrite sij; aw; rewrite LfV//. move/prl_limitP: (us) => [_ _ uv uw]; rewrite (uw _ _ lij). move:(uv _ jI) => ha; ex_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)