proposition: Lemma inl_map2_unique S S' u g g': inl_same_index S S' -> inl_map2_compat S S' u-> inl_map2_property S S' u g -> inl_map2_property S S' u g' -> g = g'.
proof: Proof. move => ha hb. move: (inl_map2_prop1 ha hb); rewrite /inl_map2_aux; set v := Lg _ _ => he. move => [g1 g2] [g3 g4]. have II:= (inl_same_index_same_I ha); rewrite II in g2 g4. have dv: domain v = (isI S') by rewrite /v; aw. have hu1: inl_map_property S v (inductive_limit S') g. split => // i idv; have ii: inc i (isI S') by ue. by rewrite - g2 // /v LgV//. have hu2: inl_map_property S v (inductive_limit S') g'. split => // i idv; have ii: inc i (isI S') by ue. rewrite - g4 // /v LgV//. exact:(inl_map_unique he hu1 hu2). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)