proposition: Lemma prl_projective_limit_fun_IV2 S1 S2 x S1' S2' x': prl_same_data S1 S1' -> prl_same_data S2 S2' -> x = x' -> projective_limit_fun S1 S2 x = projective_limit_fun S1' S2' x'.
proof: Proof. move => ha hb hc. rewrite /projective_limit_fun -hc -(projective_limit_Iv ha). have <-: (prl_map2_aux S1 x) = (prl_map2_aux S1' x). have si: (psI S1) = (psI S1'). by rewrite -!ps_substrate_r; case: ha => _ -> _. rewrite /prl_map2_aux - si; apply: Lg_exten => i ii. by rewrite (prl_can_fun_Iv i ha ). have si: (psI S2) = (psI S2') by rewrite -!ps_substrate_r; case: hb => _ -> _. by rewrite /projective_map -(projective_limit_Iv hb) /prl_map_val si. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)