proposition: Lemma prl_map_unique S u F g g': prl_map_compat S u F -> prl_map_property S u F g -> prl_map_property S u F g' -> g = g'.
proof: Proof. move => hb cp1 cp2; move:(cp1)(cp2)=>[[fg sg tg] gp] [[fg' sg' tg'] gp']. apply: function_exten => //; try ue; move => i isg /=. have isg': inc i (source g') by rewrite sg' - sg. have hu: inc (Vf g i) (projective_limit S) by rewrite - tg; fprops. have hu': inc (Vf g' i) (projective_limit S) by rewrite - tg'; fprops. move/prl_limitP:(hu) => [hc hd he hf]. move/prl_limitP:(hu') => [hc' hd' he' hf']. apply:fgraph_exten => //; rewrite hd ? hd' => // j jde. have iif: inc i F by ue. rewrite -(prl_map_property_res1 hb cp1 jde iif). by rewrite -(prl_map_property_res1 hb cp2 jde iif). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)