proposition: Lemma order_merge5 g: common_worder_axiom g -> uniqueness (common_extension_order g).
proof: Proof. move=> ca h1 h2 a1 a2;apply: (order_merge2 (order_merge3 ca) a1 a2). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)