proposition: Lemma prl_proj_image_prop3 S: prl_subfam_hyp S (prl_proj_image_fam S).
proof: Proof. rewrite/prl_proj_image_fam; split; aww. by move => i iI; rewrite LgV//; apply: prl_proj_image_prop2. move => i j lij; move: (prl_prop0 lij) => [iI jI]; rewrite !LgV//. move: (prl_can_fun_fp iI) => [fi si ti]. move: (prl_can_fun_fp jI) => [fj sj tj]. move: (ps_function_f lij); aw => - [fij sij tij]. move: (prl_proj_image_prop2 jI); rewrite - sij => hu. move => t /(Vf_image_P fij hu) [u /(Imf_P fj) ]. rewrite sj ; move => [v vl -> ->]. have axj := (prl_proj_ax jI). have axi := (prl_proj_ax iI). apply/(Imf_P fi); rewrite si; exists v => //. rewrite /prl_can_fun !LfV//; symmetry. by move/prl_limitP: vl => [ _ _ _];apply. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)