proposition: Lemma prl_map_val_aux2 S S' u (Ha :prl_same_index S S') (Hu: prl_map2_compat S S' u) (f := projective_limit_fun S S' u) i x: inc i (psI S) -> inc x (projective_limit S) -> (Vf (Vg u i) (Vg x i)) = (Vg (Vf f x) i).
proof: Proof. move => iI xs. move: (Hu) => [hu1 hu2 hu3 hu4]. move: (hu3 _ iI) => [fu su tu]. move: (prl_map2_prop Ha Hu) => [[ff sf tf] fp]. have iI': inc i (psI S') by rewrite -(prl_same_index_same_I Ha). move:(prl_proj_ax iI)(prl_proj_ax iI') => ax1 ax2. have xs2: inc x (source (projective_limit_fun S S' u)) by ue. have xs1: inc (Vg x i) (source (Vg u i)) by move:(ax1 _ xs); rewrite su. have xp1:inc (Vf (projective_limit_fun S S' u) x) (projective_limit S') by Wtac. move:(prl_can_fun_fp iI) => [fi si ti]. move:(prl_can_fun_fp iI') => [fi' si' ti']. have xs3: inc x (source (prl_can_fun S i)) by rewrite si. have co1:Vg u i \coP prl_can_fun S i by split => //; ue. move: (f_equal (Vf ^~x) (fp _ iI)). rewrite /prl_can_fun compfV // LfV // compfV //; first rewrite LfV //. split => //; ue. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)