(function_image_nonempty
 (nonempty_image 0
  (nonempty_image-1 nil 3368875322
   ("" (skosimp*)
    (("" (typepred "S!1")
      (("" (rewrite "nonempty_exists")
        (("" (rewrite "nonempty_exists")
          (("" (skosimp*)
            (("" (inst + "f!1(x!1)")
              (("" (expand "image") (("" (inst + "x!1") nil nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((nonempty? const-decl "bool" sets nil)
    (set type-eq-decl nil sets nil)
    (D formal-type-decl nil function_image_nonempty nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (image const-decl "set[R]" function_image nil)
    (R formal-type-decl nil function_image_nonempty nil)
    (x!1 skolem-const-decl "(S!1)" function_image_nonempty nil)
    (S!1 skolem-const-decl "(nonempty?[D])" function_image_nonempty
     nil)
    (f!1 skolem-const-decl "[D -> R]" function_image_nonempty nil)
    (nonempty_exists formula-decl nil sets_lemmas nil))
   nil))
 (nonempty_finite_image 0
  (nonempty_finite_image-2 nil 3368875625
   ("" (skosimp*)
    (("" (use "nonempty_image")
      (("" (expand "nonempty?") (("" (propax) nil nil)) nil)) nil))
    nil)
   ((nonempty_image judgement-tcc nil function_image_nonempty nil)
    (R formal-type-decl nil function_image_nonempty nil)
    (non_empty_finite_set type-eq-decl nil finite_sets nil)
    (empty? const-decl "bool" sets nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (is_finite const-decl "bool" finite_sets nil)
    (nonempty? const-decl "bool" sets nil)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (D formal-type-decl nil function_image_nonempty nil)
    (nonempty_image application-judgement "(nonempty?[R])"
     function_image_nonempty nil)
    (finite_image application-judgement "finite_set[R]"
     function_image_aux nil))
   nil)
  (nonempty_finite_image-1 nil 3368875322 ("" (judgement-tcc) nil nil)
   nil nil)))