proposition: Lemma prl_map2_prop3 S S' u (Ha :prl_same_index S S') (Hu: prl_map2_compat S S' u) (f := projective_limit_fun S S' u): function_prop f (projective_limit S) (projective_limit S') /\ forall 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. have ra:=(proj1 (prl_map2_prop Ha Hu)). have rb:= (prl_map_val_aux2 Ha Hu). done. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)