proposition: Lemma prl_map_property_res1 S u F g i x: prl_map_compat S u F -> prl_map_property S u F g -> inc i (psI S) -> inc x F -> Vf (Vg u i) x = Vg (Vf g x) i.
proof: Proof. move => [p1 p2 p3 p4] [[fg sg tg] hb] iI xp. rewrite p2 in hb; rewrite (hb _ iI). have xsg: inc x (source g) by rewrite sg. have vxt: inc (Vf g x) (projective_limit S) by Wtac. move:(prl_can_fun_fp iI) => [fi si ti]. have cop: prl_can_fun S i \coP g by split => //; ue. by rewrite compfV //(prl_proj_ev iI vxt). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)