theory sTs_Empty_Exist_Nitpick
imports Main
begin
declare[[show_brackets=true]]
typedecl sT
consts emS::sT
consts inS::"sT => sT => bool" (infixl "IN" 55)

axiomatization where
  eeA:"!x. \<not>(x IN emS)"

theorem emS_is_unique1:
  "!u. (!x. ~(x IN u)) --> u = emS"
  nitpick[verbose,user_axioms] oops

axiomatization where
  exA: "!u. !v. ((!x. x IN u <-> x IN v) --> u = v)"

theorem emS_is_unique2:
  "!u. (!x. ~(x IN u)) --> u = emS"
  by (metis eeA exA)
end