proposition: Lemma OT_set0: order_type_of emptyset = emptyset.
proof: Proof. move: set0_wor =>[[qa _] qb]; apply:empty_substrate_zero. ex_middle bad; move/nonemptyP: bad => [t tE]. move: (OT_prop0 qa) => [f [_ _ [[[ff _] _] sf yf] _]]. by rewrite - sf in tE;move: (Vf_target ff tE); rewrite yf qb => /in_set0. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)