(inverse_image_Union
 (inverse_image_Union 0
  (inverse_image_Union-1 nil 3389901218
   ("" (skosimp)
    (("" (apply-extensionality :hide? t)
      (("" (case-replace "inverse_image(f!1, Union(X!1))(x!1)")
        (("1" (expand "Union")
          (("1" (expand "inverse_image")
            (("1" (expand "member")
              (("1" (skosimp)
                (("1" (typepred "a!1")
                  (("1" (inst + "inverse_image(f!1,a!1)")
                    (("1" (expand "inverse_image")
                      (("1" (assert)
                        (("1" (expand "member")
                          (("1" (propax) nil nil)) nil))
                        nil))
                      nil)
                     ("2" (inst + "a!1") nil nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ("2" (assert)
          (("2" (expand "Union" -1)
            (("2" (skosimp)
              (("2" (typepred "a!1")
                (("2" (skosimp)
                  (("2" (replace -1)
                    (("2" (typepred "x!2")
                      (("2" (expand "inverse_image")
                        (("2" (expand "member")
                          (("2" (expand "Union")
                            (("2" (inst + "x!2") nil nil)) nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((S formal-type-decl nil inverse_image_Union nil)
    (boolean nonempty-type-decl nil booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (Union const-decl "set" sets nil)
    (setofsets type-eq-decl nil sets nil)
    (setof type-eq-decl nil defined_types nil)
    (inverse_image const-decl "set[D]" function_image nil)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (T formal-type-decl nil inverse_image_Union nil)
    (Union_surjective name-judgement
     "(surjective?[setofsets[T], set[T]])" sets_lemmas nil)
    (member const-decl "bool" sets nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (a!1 skolem-const-decl "(X!1)" inverse_image_Union nil)
    (f!1 skolem-const-decl "[S -> T]" inverse_image_Union nil)
    (X!1 skolem-const-decl "setofsets[T]" inverse_image_Union nil))
   shostak)))