proposition: Lemma prl_map2_unique S S' u g g': prl_same_index S S' -> prl_map2_compat S S' u-> prl_map2_property S S' u g -> prl_map2_property S S' u g' -> g = g'.
proof: Proof. move => ha hb. move: (prl_map2_prop1 ha hb); rewrite /prl_map2_aux; set v := Lg _ _ => he. move => [g1 g2] [g3 g4]. have dv: domain v = psI S by rewrite /v; aw. have hu1: prl_map_property S' v (projective_limit S) g. split => //. rewrite dv=> i idv; rewrite - g2 //; rewrite /v LgV//. have hu2: prl_map_property S' v (projective_limit S) g'. split => //; rewrite dv=> i idv; rewrite - g4 //; rewrite /v LgV//. exact:(prl_map_unique he hu1 hu2). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)