proposition: Lemma order_merge2 g: common_extension_order_axiom g -> uniqueness (common_extension_order g).
proof: Proof. move => [alo eVVg pVV] h1 h2 c1 c2. suff: (forall h1 h2, common_extension_order g h1 -> common_extension_order g h2 -> sub h1 h2). by move=> aux; apply: extensionality; apply: aux. move => r r' [or sr vr][or' sr' vr']. move=> x xr. have ppx:= (proj41 or _ xr). move:(pr1_sr xr)(pr2_sr xr); rewrite sr => pxs pys. move: (setUf_hi pxs) (setUf_hi pys)=> [u udg psu][v vdg qsv]. move:(eVVg _ _ udg vdg)=> [w [wdg wu wv]]. have: (inc x (Vg g w)). rewrite (vr _ wdg); apply /setI2_i => //;apply/setX_P;split;fprops. by rewrite (vr' _ wdg) ; move /setI2_P => []. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)