proposition: Lemma singleton_OT_pr: exists x, \1t = singleton (J x x).
proof: Proof. move: (set1_wor emptyset) => [[or _] sr]. move: (OT_prop0 or) => [f []]. rewrite sr -/singleton_order -/ singleton_OT => o1 _ fp fc. apply: set1_order_is1 => //; apply/ set_of_card_oneP. by rewrite -(cardinal_set1 emptyset); apply /card_eqP; exists f. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)