proposition: Lemma prl_proj_image_prop4 S: projective_limit S = projective_limit(projective_system_subsets (prl_proj_image_prop3 S)).
proof: Proof. move:(prl_subsets_prop (prl_proj_image_prop3 S)) => [pa pb pc pd]. move:(prl_subfam_prop1 (prl_proj_image_prop3 S)) => [_ qb _ _ _]. set_extens t. move=> tl; move/prl_limitP: (tl) => [ha hb hc hd]. have Ha i : inc i (psI S) -> inc (Vg t i) (Vg (prl_proj_image_fam S) i). move => iI; rewrite /prl_proj_image_fam ! LgV//. move: (prl_can_fun_fp iI) => [fi si ti]. apply/(Imf_P fi); rewrite si; exists t => //. have axi := (prl_proj_ax iI). rewrite /prl_can_fun LfV//. apply/prl_limitP; rewrite pa pb pc pd; split => //. move => i j lij; move:(prl_prop0 lij) => [_ jI]. by rewrite (qb _ _ _ lij (Ha _ jI)); apply: hd. move/prl_limitP => [];rewrite pa pb pc pd => ha hv hc hd. apply/prl_limitP; split => //. move => i iI; move: (hc _ iI);rewrite /prl_proj_image_fam LgV//. by apply:(prl_proj_image_prop2 iI). move => i j lij; move:(prl_prop0 lij) => [_ jI]. by move:(hd _ _ lij);rewrite /prl_proj_image_fam qb //; apply: hc. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)