fact: Definition common_extension_order g h:= [/\ order h, substrate h = unionf (domain g) (fun a => substrate (Vg g a)) & (forall a, inc a (domain g) -> order_extends (Vg g a) h)].
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)