SSL isomorphism_transitive.prf

(isomorphism_transitive
 (isomorphism_transitive 0
  (isomorphism_transitive-1 nil 3315073244
   ("" (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)
   ((O const-decl "T3" function_props nil)
    (T2 formal-type-decl nil isomorphism_transitive nil)
    (bijective? const-decl "bool" functions nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T3 formal-type-decl nil isomorphism_transitive nil)
    (T1 formal-type-decl nil isomorphism_transitive 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)
    (isomorphism? const-decl "bool" isomorphism nil))
   shostak)))