proposition: Lemma prl_proj_image_prop2 S i: inc i (psI S) -> sub (prl_proj_image S i) (Vg (psE S) i).
proof: Proof. move => iI. move: (prl_can_fun_fp iI) => [ff sf tf]. move => t /(Imf_P ff); rewrite sf; move => [u up -> ]. have ax := (prl_proj_ax iI). move/prl_limitP: (up) => [_ _ uv _]. by rewrite /prl_can_fun LfV//; apply: uv. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)