proposition: Lemma prl_inv_hyp_prop S S' u x (Hsb: prl_same_index S S') (Hc: prl_map2_compat S S' u) (Hx: inc x (projective_limit S')): (Vfi1 (projective_limit_fun S S' u) x) = projective_limit (projective_system_subsets (prl_inv_hyp Hsb Hc Hx)).
proof: Proof. rewrite prl_subsets_prop2. move: (prl_map2_prop Hsb Hc); set pu := (projective_limit_fun S S' u). move => [[fpu spu tpu] pup]. move:(prl_inv_hyp Hsb Hc Hx) =>[]; set g := (prl_invim_set u x). move => fgg dg gp1 gp2. move:(Hc) => [fgu du up1 up2]. have ax1:= (prl_map_ax (prl_map2_prop1 Hsb Hc)). have ssI: psI S = psI S' := prl_same_index_same_I Hsb. set_extens t. move/(iim_fun_set1_P _ fpu) => [ts xv]; rewrite spu in ts. apply/setI2_P; split => //. move: xv; rewrite /pu /projective_limit_fun /projective_map /prl_map_val. aw; move => xv. move/prl_limitP: (ts) => [fgt st tv tp2]. have dtdg: domain t = domain g by rewrite st dg. apply/setXb_P;split => //. rewrite dg; move => i idg. have iI': inc i (psI S') by ue. have idu: inc i (domain u) by ue. rewrite /g /prl_invim_set LgV//. move: (up1 _ idg) => [fui sui tui]. apply/(iim_fun_set1_P _ fui); rewrite sui; split => //. by apply: tv. by rewrite xv LfV // LgV//; apply: prl_map2_prop2. move/setI2_P =>[ha hb]. apply/(iim_fun_set1_P _ fpu); rewrite spu; split => //. rewrite /pu /projective_limit_fun /projective_map LfV//. move/prl_limitP:(Hx) => [fgx dx xv xp]. rewrite /prl_map_val. apply:fgraph_exten. + done. + fprops. + by aw. + rewrite dx => i iI'. move:(iI'); rewrite - ssI => iI. have idu: inc i (domain u) by ue. move: (up1 _ iI) => [fui sui tui]. move/setXb_P: hb => [ft dt tv]. have idg: inc i (domain g) by rewrite dg. move: (tv _ idg); rewrite /g /prl_invim_set LgV//. by case/(iim_fun_set1_P _ fui) => _ ->; rewrite LgV // prl_map2_prop2. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)