proposition: Lemma ex9_map_unique g g': ex9_map_property g -> ex9_map_property g' -> g = g'.
proof: Proof. move => hb hc. move:(proj1 hb) (proj1 hc) => [fg sg tg] [fg' sg' tg']. apply: function_exten => //; try ue. move: (chain_equivalence_eq) => [eqv seq]. rewrite sg => x /ex9_quoP [rs ->]. move: rs; rewrite seq => /ex9G_P [pr p1 p2]. rewrite - pr. by rewrite (ex9_map_property_res1 hb p1 p2) (ex9_map_property_res1 hc p1 p2). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)