proposition: Lemma prl_map2_compat_aux S S' u x i j: prl_same_index S S' -> prl_map2_compat S S' u -> inc x (projective_limit S) -> gle (psr S) i j -> Vf (Vg u i) (Vg x i) = Vf (Vg (psf S') (J i j)) (Vf (Vg u j) (Vg x j)).
proof: Proof. move => ha [hb1 hb2 hb3 hb4] /prl_limitP [fgx dx xv xw] lij. move: (prl_prop0 lij) => [iI jI]. have lij': gle (psr S') i j by rewrite - ha. move: (hb3 _ iI) => [fui sui tui]. move: (hb3 _ jI) => [fuj suj tuj]. move: (ps_function_f lij) => [fij sij tij]. move: (ps_function_f lij') => [fij' sij' tij']. have co1: Vg u i \coP Vg (psf S) (J i j) by split => //; rewrite sui tij; aw. have co2: Vg (psf S') (J i j) \coP Vg u j by split => //; rewrite sij' tuj;aw. have xs1: inc (Vg x j) (source (Vg u j)) by rewrite suj; apply: xv. have xs2: inc (Vg x j) (source (Vg (psf S) (J i j))). by rewrite sij pr2_pair;apply: xv. move: (f_equal (Vf ^~(Vg x j)) (hb4 _ _ lij)). by rewrite !compfV//; move <-; rewrite - (xw _ _ lij). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)