proposition: Lemma prl_dirim_prop S S' u (Hsb: prl_same_index S S') (Hc: prl_map2_compat S S' u): sub (Imf (projective_limit_fun S S' u)) (projective_limit (projective_system_subsets (prl_direct_hyp Hsb Hc))).
proof: Proof. move => t. move:(prl_map2_prop Hsb Hc) =>[ [fp sp tp] _]. move/(Imf_P fp) =>[x xt ->]. move: xt;rewrite sp => xd; move: (xd)=> /prl_limitP [fgx dx xv xp]. move: (prl_map_ax (prl_map2_prop1 Hsb Hc)) => ax. rewrite /projective_limit_fun/projective_map LfV//. rewrite /projective_limit /=. set v := (prl_map_val S' (prl_map2_aux S u) x). move:(Hc) => [hc1 hc2 hc3 hc4]. have ssI := prl_same_index_same_I Hsb. apply/Zo_P; split. apply/setXb_P; rewrite /v/prl_map_val/prl_dirim_set; split. - fprops. - by aw; rewrite hc2 ssI. - aw; rewrite hc2; move => i iI. have iI': inc i (psI S') by rewrite - ssI. move:(hc3 _ iI) =>[fui sui tui]. have aux: inc (Vg x i) (source (Vg u i)). by rewrite sui; apply: xv. rewrite LgV// (prl_map2_prop2 iI xd fui sui) LgV//. by apply/(Imf_P fui); ex_tac. move => i j lij. move:(prl_prop0 lij) =>[iI' jI']. have iI: inc i (psI S) by rewrite ssI. have jI: inc j (psI S) by rewrite ssI. move:(hc3 _ iI) =>[fui sui tui]. move:(hc3 _ jI) =>[fuj suj tuj]. have jdu: inc j (domain u) by rewrite hc2. have aux: inc (Vg x j) (source (Vg u j)) by rewrite suj; apply: xv. rewrite /v/prl_map_val LgV//. rewrite (prl_map2_prop2 iI xd fui sui). rewrite LgV// (prl_map2_prop2 jI xd fuj suj). have hu: inc (Vf (Vg u j) (Vg x j)) (Vg (prl_dirim_set u) j). rewrite /prl_dirim_set LgV//. apply/(Imf_P fuj); ex_tac. move:(prl_subfam_prop1 (prl_direct_hyp Hsb Hc)) => [_ k2 _ _ _]; rewrite k2 //. rewrite -Hsb in lij;exact: (prl_map2_compat_aux Hsb Hc xd lij). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)