proposition: Lemma prl_map2_prop1 S S' u: prl_same_index S S' -> prl_map2_compat S S' u -> prl_map_compat S' (prl_map2_aux S u) (projective_limit S).
proof: Proof. move => pa [pd pe pf pg]. have ha:= (prl_same_index_same_I pa). rewrite /prl_map2_aux; split; aww. move => i iI; rewrite LgV//. move:(pf _ iI) => [fui sui tui]. move:(prl_can_fun_fp iI) => [fp sp tp]. by saw; fct_tac; rewrite sui. move => i j le1. have le2: gle (psr S) i j by rewrite pa. move: (prl_prop0 le2) => [isr jsr]. move : (pf _ isr) => [fui sui tui]. move : (pf _ jsr) => [fuj suj tuj]. move: (ps_function_f le2) => [fa sfa tga]. move: (ps_function_f le1) => [fa' sfa' tga']. have cp1: Vg (psf S') (J i j) \coP Vg u j. by split => //; rewrite sfa' tuj; aw. rewrite - pa in le1;move:(prl_can_fun_fp jsr) => [ ha' hb hc]. have cp2:Vg u j \coP prl_can_fun S j. by split => //; rewrite hc. have cp3: Vg u i \coP Vg (psf S) (J i j). by split => //; rewrite tga sui; aw. move: (prl_can_fun_prop le1) => [hd he]. by rewrite !LgV// compfA // - (pg _ _ le1) - compfA // - he. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)