(vect_fun_ops_rv
 (diff_function 0
  (diff_function-1 nil 3471883199
   ("" (skosimp*)
    (("" (expand "-")
      (("" (apply-extensionality 1 :hide? t)
        (("" (expand "+ ") (("" (propax) nil nil)) nil)) nil))
      nil))
    nil)
   ((- const-decl "Vector" vectors_2D "vectors/")
    (- const-decl "Vector" vectors_2D "vectors/")
    (minus_real_is_real application-judgement "real" reals nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (Vect2 type-eq-decl nil vectors_2D_def "vectors/")
    (+ const-decl "Vector" vectors_2D "vectors/")
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (Vector type-eq-decl nil vectors_2D "vectors/")
    (real nonempty-type-from-decl nil reals nil)
    (T formal-type-decl nil vect_fun_ops_rv nil))
   shostak))
 (negneg_function 0
  (negneg_function-1 nil 3471883231
   ("" (skosimp*)
    (("" (expand "-")
      (("" (apply-extensionality :hide? t)
        (("" (apply-extensionality 1 :hide? t) nil nil)) nil))
      nil))
    nil)
   ((- const-decl "Vector" vectors_2D "vectors/")
    (minus_real_is_real application-judgement "real" reals nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (Vect2 type-eq-decl nil vectors_2D_def "vectors/")
    (Vector type-eq-decl nil vectors_2D "vectors/")
    (real nonempty-type-from-decl nil reals nil)
    (T formal-type-decl nil vect_fun_ops_rv nil))
   shostak)))