proposition: Lemma inl_map_unique S u F g g': inl_map_compat S u F -> inl_map_property S u F g -> inl_map_property S u F g' -> g = g'.
proof: Proof. move => ha hb hc. have seqv:=(inl_equiv_sr S). move:(proj1 hb) (proj1 hc) => [fg sg tg] [fg' sg' tg']. apply: function_exten => //; try ue. rewrite sg => x /inductive_limitP [rs ->]. move: rs; rewrite seqv => /inl_sumP [pr p1 p2]. rewrite - pr. rewrite (inl_map_property_res1 ha hb p1 p2). by rewrite (inl_map_property_res1 ha hc p1 p2). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)