proposition: Lemma prl_inv_hyp S S' u x: prl_same_index S S' -> prl_map2_compat S S' u -> inc x (projective_limit S') -> prl_subfam_hyp S (prl_invim_set u x).
proof: Proof. move => ha[pa pb pc pd] /prl_limitP[fgx dx vx wx]. have ssI:=prl_same_index_same_I ha. rewrite/prl_invim_set; split=> //; fprops; aw; trivial. move => i iS. move: (pc _ iS) => [fu su tu]. have ra: sub (singleton (Vg x i)) (target (Vg u i)). by move => t /set1_P ->; rewrite tu; apply: vx; rewrite - ssI. rewrite - pb in iS; rewrite LgV //- su; exact:(sub_inv_im_source fu ra). move => i j lij. move:(prl_prop0 lij)=> [idu jdu]. move: (pc _ idu) => [fui sui tui]. move: (pc _ jdu) => [fuj suj tuj]. move: (ps_function_f lij) => [ff sf tf]. have jde: inc j (domain (psE S')) by rewrite ps_domain_E - ssI. have si1: sub (Vfi1 (Vg u j) (Vg x j)) (source (Vg (psf S) (J i j))). rewrite sf pr2_pair - suj; apply:(sub_inv_im_source fuj). by move => t /set1_P ->; rewrite tuj; apply: vx; rewrite - ssI. move: (lij); rewrite ha => lij'. move: (ps_function_f lij') => [ff' sf' tf']. rewrite pr1_pair in tf; rewrite pr2_pair in sf. rewrite pr1_pair in tf'; rewrite pr2_pair in sf'. have co1: Vg (psf S') (J i j) \coP Vg u j by split => //;rewrite sf' tuj. have co2: Vg u i \coP Vg (psf S) (J i j) by split => //;rewrite tf sui. rewrite !LgV// ? pb//; move => t. move/(Vf_image_P ff si1) => [z /(iim_fun_set1_P _ fuj) [za zb] ->]. apply/(iim_fun_set1_P _ fui); split. by rewrite sui - tf; Wtac; rewrite sf - suj. move /(f_equal (Vf^~z)) :(pd _ _ lij); rewrite !compfV//. by move => ->; rewrite - zb; apply: wx. by rewrite sf - suj. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)