proposition: Lemma prl_map2_prop2 S u i t: inc i (psI S) -> inc t (projective_limit S) -> function (Vg u i) -> source (Vg u i) = Vg (psE S) i -> Vf (Vg (prl_map2_aux S u) i) t = Vf (Vg u i) (Vg t i).
proof: Proof. move => iI tlim fu su. move: (prl_can_fun_fp iI) => [ff sf tf]. have tl: inc t (source (prl_can_fun S i)) by ue. have hh: Vg u i \coP prl_can_fun S i. by split => //; rewrite tf. by rewrite /prl_map2_aux LgV// compfV// prl_proj_ev. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)