proposition: Lemma prl_map2_prop S S' u (g := projective_limit_fun S S' u): prl_same_index S S' -> prl_map2_compat S S' u -> prl_map2_property S S' u g.
proof: Proof. move => ha hb. move:(prl_map2_prop1 ha hb); set v := (prl_map2_aux S u) => hc. move: (prl_map_prop hc); rewrite /v -/(projective_limit_fun _ _ _) -/g. move => [qa qb]. split => // i iI. have idx: inc i (domain (prl_map2_aux S u)) by rewrite /prl_map2_aux; aw. by rewrite - qb // /prl_map2_aux LgV. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)