(isomorphism_equivalence
 (isomorphism_reflexive 0
  (isomorphism_reflexive-1 nil 3315072687
   ("" (grind)
    (("" (inst + "identity[T]")
      (("" (expand "identity") (("" (propax) nil nil)) nil)) nil))
    nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (bijective? const-decl "bool" functions nil)
    (identity const-decl "(bijective?[T, T])" identity nil)
    (reflexive? const-decl "bool" relations nil)
    (isomorphic? const-decl "bool" isomorphism nil)
    (isomorphism? const-decl "bool" isomorphism nil)
    (T formal-type-decl nil isomorphism_equivalence nil))
   shostak))
 (isomorphism_symmetric 0
  (isomorphism_symmetric-1 nil 3315072724
   ("" (expand* "isomorphic?" "isomorphism?" "symmetric?")
    (("" (skosimp* t)
      (("" (use "bijective_inverse_exists")
        (("" (expand "exists1")
          (("" (skosimp*)
            (("" (assert)
              (("" (lemma "bij_inv_is_bij_alt" ("f" "f!1" "g" "x!2"))
                (("" (inst + "x!2")
                  (("" (skolem!)
                    (("" (inst - "x!2(d1!1)" "x!2(d2!1)")
                      (("" (expand "inverse?")
                        (("" (inst-cp - "d2!1")
                          (("" (inst - "d1!1")
                            (("" (split)
                              (("1"
                                (split)
                                (("1" (ground) nil nil)
                                 ("2"
                                  (expand* "bijective?" "surjective?")
                                  (("2"
                                    (flatten)
                                    (("2" (inst -6 "d2!1") nil nil))
                                    nil))
                                  nil))
                                nil)
                               ("2"
                                (expand* "bijective?" "surjective?")
                                (("2"
                                  (flatten)
                                  (("2" (inst -6 "d1!1") nil nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((bijective? const-decl "bool" functions nil)
    (T formal-type-decl nil isomorphism_equivalence nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (exists1 const-decl "bool" exists1 nil)
    (x!2 skolem-const-decl "[T -> T]" isomorphism_equivalence nil)
    (surjective? const-decl "bool" functions nil)
    (inverse? const-decl "bool" function_inverse_def nil)
    (bij_inv_is_bij_alt formula-decl nil function_inverse_def nil)
    (bijective_inverse_exists formula-decl nil function_inverse_def
     nil)
    (isomorphic? const-decl "bool" isomorphism nil)
    (symmetric? const-decl "bool" relations nil)
    (isomorphism? const-decl "bool" isomorphism nil))
   shostak))
 (isomorphism_transitive 0
  (isomorphism_transitive-1 nil 3315072868
   ("" (expand* "isomorphic?" "isomorphism?" "transitive?")
    (("" (skosimp*)
      (("" (inst + "f!2 o f!1")
        (("" (skolem!)
          (("" (inst?)
            (("" (inst?) (("" (expand "o") (("" (prop) nil nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((T formal-type-decl nil isomorphism_equivalence nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (bijective? const-decl "bool" functions nil)
    (O const-decl "T3" function_props nil)
    (composition_bijective application-judgement "(bijective?[T1, T3])"
     function_props nil)
    (composition_surjective application-judgement
     "(surjective?[T1, T3])" function_props nil)
    (composition_injective application-judgement "(injective?[T1, T3])"
     function_props nil)
    (isomorphic? const-decl "bool" isomorphism nil)
    (transitive? const-decl "bool" relations nil)
    (isomorphism? const-decl "bool" isomorphism nil))
   shostak))
 (isomorphism_equivalence 0
  (isomorphism_equivalence-1 nil 3315072679
   ("" (expand "equivalence?")
    (("" (lemma "isomorphism_reflexive")
      (("" (lemma "isomorphism_symmetric")
        (("" (lemma "isomorphism_transitive") (("" (assert) nil nil))
          nil))
        nil))
      nil))
    nil)
   ((isomorphism_reflexive formula-decl nil isomorphism_equivalence
     nil)
    (isomorphism_transitive formula-decl nil isomorphism_equivalence
     nil)
    (isomorphism_symmetric formula-decl nil isomorphism_equivalence
     nil)
    (equivalence? const-decl "bool" relations nil))
   nil)))