(compact_spaces
 (compact_closed_def 0
  (compact_closed_def-1 nil 3406967481
   ("" (skosimp)
    (("" (typepred "S")
      (("" (rewrite "compact_def")
        (("" (inst - "U!1") (("" (assert) nil nil)) nil)) nil))
      nil))
    nil)
   ((S formal-const-decl "compact_space" compact_spaces nil)
    (compact_space nonempty-type-eq-decl nil topology_prelim nil)
    (compact_space? const-decl "bool" topology_prelim nil)
    (setofsets type-eq-decl nil sets nil)
    (setof type-eq-decl nil defined_types nil)
    (T formal-type-decl nil compact_spaces nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (Intersection_surjective name-judgement
     "(surjective?[setofsets[T], set[T]])" sets_lemmas nil)
    (compact_def formula-decl nil topology nil))
   shostak)))