(homeomorphic_reflexive
 (homeomorphic_reflexive 0
  (homeomorphic_reflexive-1 nil 3301321662
   ("" (expand "homeomorphic?")
    (("" (inst + "lambda (x:T): x")
      (("" (expand "homeomorphism?")
        (("" (case-replace "continuous?[T, S, T, S](LAMBDA (x: T): x)")
          (("1" (case-replace "bijective?[T, T](LAMBDA (x: T): x)")
            (("1" (case "EXISTS (x:T): TRUE")
              (("1"
                (case-replace
                 "inverse_alt(LAMBDA (x: T): x) = (LAMBDA (x: T): x)")
                (("1" (hide 2)
                  (("1" (hide -3)
                    (("1"
                      (lemma "bijective_inverse_is_inverse_alt"
                       ("f" "LAMBDA (x: T): x" "g"
                        "(LAMBDA (x: T): x)"))
                      (("1" (replace -1 1 rl) (("1" (propax) nil nil))
                        nil)
                       ("2" (hide 2)
                        (("2" (expand "inverse?")
                          (("2" (propax) nil nil)) nil))
                        nil)
                       ("3" (propax) nil nil) ("4" (flatten) nil nil))
                      nil))
                    nil))
                  nil)
                 ("2" (flatten) nil nil))
                nil)
               ("2" (expand "continuous?")
                (("2" (skosimp*) (("2" (inst + "x!1") nil nil)) nil))
                nil))
              nil)
             ("2" (hide-all-but 1)
              (("2" (expand "bijective?")
                (("2" (expand "injective?")
                  (("2" (expand "surjective?")
                    (("2" (split)
                      (("1" (skosimp) nil nil)
                       ("2" (skosimp) (("2" (inst + "y!1") nil nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil)
           ("2" (hide 2)
            (("2" (expand "continuous?")
              (("2" (expand "continuous_at?")
                (("2" (expand "inverse_image")
                  (("2" (skosimp*)
                    (("2" (expand "neighbourhood?")
                      (("2" (expand "interior_point?")
                        (("2" (skosimp*)
                          (("2" (inst + "U!2")
                            (("2" (assert)
                              (("2"
                                (expand "subset?")
                                (("2"
                                  (skosimp*)
                                  (("2"
                                    (inst - "x!2")
                                    (("2" (assert) nil nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((T formal-type-decl nil homeomorphic_reflexive nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (setof type-eq-decl nil defined_types nil)
    (setofsets type-eq-decl nil sets nil)
    (topology? const-decl "bool" topology_prelim nil)
    (topology nonempty-type-eq-decl nil topology_prelim nil)
    (S formal-const-decl "topology[T]" homeomorphic_reflexive nil)
    (continuous? const-decl "bool" continuity_def nil)
    (injective? const-decl "bool" functions nil)
    (surjective? const-decl "bool" functions nil)
    (TRUE const-decl "bool" booleans nil)
    (bijective_inverse_is_inverse_alt formula-decl nil
     function_inverse_alt nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (inverse? const-decl "bool" function_inverse_def nil)
    (inverses nonempty-type-eq-decl nil function_inverse_alt nil)
    (inverse_alt const-decl "inverses(f)" function_inverse_alt nil)
    (FALSE const-decl "bool" booleans nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (bijective? const-decl "bool" functions nil)
    (inverse_image const-decl "set[D]" function_image nil)
    (neighbourhood? const-decl "bool" topology nil)
    (subset_is_partial_order name-judgement "(partial_order?[set[T]])"
     sets_lemmas nil)
    (member const-decl "bool" sets nil)
    (subset? const-decl "bool" sets nil)
    (set type-eq-decl nil sets nil)
    (open? const-decl "bool" topology nil)
    (open nonempty-type-eq-decl nil topology nil)
    (interior_point? const-decl "bool" topology nil)
    (continuous_at? const-decl "bool" continuity_def nil)
    (homeomorphism? const-decl "bool" homeomorphism_def nil)
    (homeomorphic? const-decl "bool" homeomorphism_def nil))
   shostak)))