(deriv_sincos_ax
 (sin_derivable_TCC1 0
  (sin_derivable_TCC1-1 nil 3476447874
   ("" (lemma "connected_deriv_domain[T]") (("" (assert) nil nil)) nil)
   ((connected_domain formula-decl nil deriv_sincos_ax nil)
    (not_one_element formula-decl nil deriv_sincos_ax nil)
    (connected_deriv_domain formula-decl nil deriv_domain_def
     "analysis/")
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (T_pred const-decl "[real -> boolean]" deriv_sincos_ax nil)
    (T formal-subtype-decl nil deriv_sincos_ax nil))
   nil))
 (sin_derivable_TCC2 0
  (sin_derivable_TCC2-1 nil 3476447874
   ("" (assert)
    (("" (skosimp*)
      (("" (lemma "not_one_element")
        (("" (assert)
          (("" (expand "not_one_element?") (("" (inst?) nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((not_one_element formula-decl nil deriv_sincos_ax nil)) nil))
 (deriv_sin_TCC1 0
  (deriv_sin_TCC1-1 nil 3476447874
   ("" (skosimp*)
    (("" (lemma "sin_derivable") (("" (inst?) nil nil)) nil)) nil)
   ((sin_derivable formula-decl nil deriv_sincos_ax 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)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil))
   nil))
 (deriv_cos_TCC1 0
  (deriv_cos_TCC1-1 nil 3476447874
   ("" (skosimp*)
    (("" (lemma "cos_derivable") (("" (inst?) nil nil)) nil)) nil)
   ((cos_derivable formula-decl nil deriv_sincos_ax 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)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil))
   nil)))