proposition: Lemma prl_proj_image_fam_fs S (fij' := prl_subfam_fct S (prl_proj_image_fam S)): forall ij, inc ij (psr S) -> surjection (Vg fij' ij).
proof: Proof. move => ij ijr. move:(prl_subfam_prop1 (prl_proj_image_prop3 S)). rewrite -/fij'; move => [p1 p2 p3 p4 p5]. move:(p3 ij ijr) => [fij sij tij]; split => //. move:(pr1_sr ijr) (pr2_sr ijr); rewrite ps_substrate_r => iI jI. rewrite sij tij /prl_proj_image_fam LgV// LgV//. move: ((proj31 (ps_preorder_r S)) _ ijr) => pij. move: (prl_can_fun_fp iI) => [fi si ti]. move: (prl_can_fun_fp jI) => [fj sj tj]. move => y /(Imf_P fi); rewrite si => - [u up ->]. have axi := (prl_proj_ax iI). have axj := (prl_proj_ax jI). have ra: inc (Vg u (Q ij)) (Imf (prl_can_fun S (Q ij))). apply /(Imf_P fj); rewrite sj. exists u => //; rewrite /prl_can_fun LfV//. exists (Vg u (Q ij)) => //. have rb: inc (Vg u (Q ij)) (Vg (prl_proj_image_fam S) (Q ij)). rewrite /prl_proj_image_fam ! LgV//. rewrite - pij in ijr; move: (p2 _ _ (Vg u (Q ij)) ijr rb); rewrite{1} pij => ->. rewrite /prl_can_fun LfV//. by move/prl_limitP: up => [_ _ _ h]; rewrite - h. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)