(finite_fubini_scaf
 (mu_TCC1 0
  (mu_TCC1-1 nil 3458551591
   ("" (typepred "S1")
    (("" (expand "sigma_algebra?")
      (("" (expand "subset_algebra_empty?")
        (("" (flatten)
          (("" (expand "member") (("" (propax) nil nil)) nil)) nil))
        nil))
      nil))
    nil)
   ((member const-decl "bool" sets nil)
    (subset_algebra_empty? const-decl "bool" subset_algebra_def nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (T1 formal-type-decl nil finite_fubini_scaf nil)
    (setof type-eq-decl nil defined_types nil)
    (setofsets type-eq-decl nil sets nil)
    (sigma_algebra? const-decl "bool" subset_algebra_def nil)
    (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
    (S1 formal-const-decl "sigma_algebra[T1]" finite_fubini_scaf nil))
   nil))
 (nu_TCC1 0
  (nu_TCC1-1 nil 3458551591
   ("" (typepred "S2")
    (("" (expand "sigma_algebra?")
      (("" (expand "subset_algebra_empty?")
        (("" (flatten)
          (("" (expand "member") (("" (propax) nil nil)) nil)) nil))
        nil))
      nil))
    nil)
   ((member const-decl "bool" sets nil)
    (subset_algebra_empty? const-decl "bool" subset_algebra_def nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (T2 formal-type-decl nil finite_fubini_scaf nil)
    (setof type-eq-decl nil defined_types nil)
    (setofsets type-eq-decl nil sets nil)
    (sigma_algebra? const-decl "bool" subset_algebra_def nil)
    (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
    (S2 formal-const-decl "sigma_algebra[T2]" finite_fubini_scaf nil))
   nil))
 (measurable_x_section 0
  (measurable_x_section-1 nil 3458807198
   ("" (skosimp)
    (("" (typepred "m!1")
      (("" (rewrite "measurable_gt")
        (("" (rewrite "measurable_gt")
          (("" (skosimp)
            (("" (inst - "c!1")
              ((""
                (lemma "x_section_measurable"
                 ("S1" "S1" "S2" "S2" "Z"
                  "{z: [T1, T2] | m!1(z) > c!1}" "x" "x!1"))
                (("" (expand "member")
                  (("" (assert)
                    (("" (expand "x_section") (("" (propax) nil nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((measurable_function nonempty-type-eq-decl nil measure_space_def
     nil)
    (measurable_function? const-decl "bool" measure_space_def nil)
    (S2 formal-const-decl "sigma_algebra[T2]" finite_fubini_scaf nil)
    (S1 formal-const-decl "sigma_algebra[T1]" finite_fubini_scaf nil)
    (sigma_times const-decl "sigma_algebra[[T1, T2]]" product_sigma_def
     nil)
    (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
    (sigma_algebra? const-decl "bool" subset_algebra_def nil)
    (setofsets type-eq-decl nil sets nil)
    (setof type-eq-decl nil defined_types nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number nonempty-type-decl nil numbers nil)
    (T2 formal-type-decl nil finite_fubini_scaf nil)
    (T1 formal-type-decl nil finite_fubini_scaf nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (member const-decl "bool" sets nil)
    (x_section const-decl "set[T2]" cross_product "topology/")
    (x_section_measurable formula-decl nil product_sigma_def nil)
    (set type-eq-decl nil sets nil) (> const-decl "bool" reals nil)
    (measurable_gt formula-decl nil measure_space_def nil))
   shostak))
 (measurable_y_section 0
  (measurable_y_section-1 nil 3458807343
   ("" (skosimp)
    (("" (typepred "m!1")
      (("" (rewrite "measurable_gt")
        (("" (rewrite "measurable_gt")
          (("" (skosimp)
            (("" (inst - "c!1")
              ((""
                (lemma "y_section_measurable"
                 ("S1" "S1" "S2" "S2" "Z"
                  "{z: [T1, T2] | m!1(z) > c!1}" "y" "y!1"))
                (("" (expand "member")
                  (("" (assert)
                    (("" (expand "y_section") (("" (propax) nil nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((measurable_function nonempty-type-eq-decl nil measure_space_def
     nil)
    (measurable_function? const-decl "bool" measure_space_def nil)
    (S2 formal-const-decl "sigma_algebra[T2]" finite_fubini_scaf nil)
    (S1 formal-const-decl "sigma_algebra[T1]" finite_fubini_scaf nil)
    (sigma_times const-decl "sigma_algebra[[T1, T2]]" product_sigma_def
     nil)
    (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
    (sigma_algebra? const-decl "bool" subset_algebra_def nil)
    (setofsets type-eq-decl nil sets nil)
    (setof type-eq-decl nil defined_types nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number nonempty-type-decl nil numbers nil)
    (T2 formal-type-decl nil finite_fubini_scaf nil)
    (T1 formal-type-decl nil finite_fubini_scaf nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (member const-decl "bool" sets nil)
    (y_section const-decl "set[T1]" cross_product "topology/")
    (y_section_measurable formula-decl nil product_sigma_def nil)
    (set type-eq-decl nil sets nil) (> const-decl "bool" reals nil)
    (measurable_gt formula-decl nil measure_space_def nil))
   shostak))
 (isf_x_section 0
  (isf_x_section-1 nil 3458807584
   ("" (skosimp)
    (("" (typepred "i!1")
      (("" (expand "isf?")
        (("" (flatten)
          (("" (expand "simple?")
            (("" (flatten)
              (("" (expand "mu_fin?")
                (("" (expand "to_measure")
                  (("" (hide -3)
                    ((""
                      (lemma "finite_subset[real]"
                       ("A" "image(i!1, fullset[[T1, T2]])" "s"
                        "image(LAMBDA y: i!1(x!1, y), fullset[T2])"))
                      (("1" (assert)
                        (("1" (split)
                          (("1" (assert)
                            (("1" (hide -1 -3)
                              (("1"
                                (lemma
                                 "measurable_x_section"
                                 ("m" "i!1" "x" "x!1"))
                                (("1" (propax) nil nil))
                                nil))
                              nil))
                            nil)
                           ("2" (hide-all-but 1)
                            (("2" (expand "fullset")
                              (("2"
                                (expand "image")
                                (("2"
                                  (expand "subset?")
                                  (("2"
                                    (expand "member")
                                    (("2"
                                      (skosimp*)
                                      (("2"
                                        (inst + "(x!1,x!3)")
                                        nil
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil)
                       ("2" (propax) nil nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((isf nonempty-type-eq-decl nil isf nil)
    (isf? const-decl "bool" isf nil)
    (nu formal-const-decl "finite_measure[T2, S2]" finite_fubini_scaf
     nil)
    (mu formal-const-decl "finite_measure[T1, S1]" finite_fubini_scaf
     nil)
    (fm_times const-decl
     "finite_measure[[T1, T2], sigma_times(S1, S2)]"
     product_finite_measure nil)
    (to_measure const-decl "measure_type" generalized_measure_def nil)
    (measure_type nonempty-type-eq-decl nil generalized_measure_def
     nil)
    (measure? const-decl "bool" generalized_measure_def nil)
    (extended_nnreal nonempty-type-eq-decl nil extended_nnreal
     "extended_nnreal/")
    (finite_measure nonempty-type-eq-decl nil generalized_measure_def
     nil)
    (finite_measure? const-decl "bool" generalized_measure_def nil)
    (nnreal type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (S2 formal-const-decl "sigma_algebra[T2]" finite_fubini_scaf nil)
    (S1 formal-const-decl "sigma_algebra[T1]" finite_fubini_scaf nil)
    (sigma_times const-decl "sigma_algebra[[T1, T2]]" product_sigma_def
     nil)
    (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
    (sigma_algebra? const-decl "bool" subset_algebra_def nil)
    (setofsets type-eq-decl nil sets nil)
    (setof type-eq-decl nil defined_types nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number nonempty-type-decl nil numbers nil)
    (T2 formal-type-decl nil finite_fubini_scaf nil)
    (T1 formal-type-decl nil finite_fubini_scaf nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (measurable_fullset name-judgement "measurable_set[T, S]"
     finite_fubini_scaf nil)
    (subset_algebra_fullset name-judgement "(S)" finite_fubini_scaf
     nil)
    (measurable_fullset name-judgement "measurable_set[T, S]"
     finite_fubini_scaf nil)
    (subset_algebra_fullset name-judgement "(S)" finite_fubini_scaf
     nil)
    (finite_subset formula-decl nil finite_sets nil)
    (set type-eq-decl nil sets nil)
    (is_finite const-decl "bool" finite_sets nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (image const-decl "set[R]" function_image nil)
    (fullset const-decl "set" sets nil)
    (measurable_function nonempty-type-eq-decl nil measure_space_def
     nil)
    (measurable_function? const-decl "bool" measure_space_def nil)
    (measurable_x_section formula-decl nil finite_fubini_scaf nil)
    (subset? const-decl "bool" sets nil)
    (TRUE const-decl "bool" booleans nil)
    (member const-decl "bool" sets nil)
    (subset_is_partial_order name-judgement "(partial_order?[set[T]])"
     sets_lemmas nil)
    (subset_is_partial_order name-judgement "(partial_order?[set[T]])"
     sets_lemmas_aux nil)
    (mu_fin? const-decl "bool" measure_props nil)
    (simple? const-decl "bool" measure_space nil))
   shostak))
 (isf_y_section 0
  (isf_y_section-1 nil 3458807902
   ("" (skosimp)
    (("" (typepred "i!1")
      (("" (expand "isf?")
        (("" (expand "simple?")
          (("" (flatten)
            (("" (lemma "measurable_y_section" ("y" "y!1" "m" "i!1"))
              (("" (assert)
                (("" (expand "mu_fin?")
                  (("" (expand "to_measure")
                    (("" (hide-all-but (-3 1))
                      ((""
                        (lemma "finite_subset[real]"
                         ("A" "image(i!1, fullset[[T1, T2]])" "s"
                          "image(LAMBDA x: i!1(x, y!1), fullset[T1])"))
                        (("" (assert)
                          (("" (hide-all-but 1)
                            (("" (expand "fullset")
                              ((""
                                (expand "image")
                                ((""
                                  (expand "subset?")
                                  ((""
                                    (expand "member")
                                    ((""
                                      (skosimp*)
                                      ((""
                                        (inst + "(x!2, y!1)")
                                        nil
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((isf nonempty-type-eq-decl nil isf nil)
    (isf? const-decl "bool" isf nil)
    (nu formal-const-decl "finite_measure[T2, S2]" finite_fubini_scaf
     nil)
    (mu formal-const-decl "finite_measure[T1, S1]" finite_fubini_scaf
     nil)
    (fm_times const-decl
     "finite_measure[[T1, T2], sigma_times(S1, S2)]"
     product_finite_measure nil)
    (to_measure const-decl "measure_type" generalized_measure_def nil)
    (measure_type nonempty-type-eq-decl nil generalized_measure_def
     nil)
    (measure? const-decl "bool" generalized_measure_def nil)
    (extended_nnreal nonempty-type-eq-decl nil extended_nnreal
     "extended_nnreal/")
    (finite_measure nonempty-type-eq-decl nil generalized_measure_def
     nil)
    (finite_measure? const-decl "bool" generalized_measure_def nil)
    (nnreal type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (S2 formal-const-decl "sigma_algebra[T2]" finite_fubini_scaf nil)
    (S1 formal-const-decl "sigma_algebra[T1]" finite_fubini_scaf nil)
    (sigma_times const-decl "sigma_algebra[[T1, T2]]" product_sigma_def
     nil)
    (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
    (sigma_algebra? const-decl "bool" subset_algebra_def nil)
    (setofsets type-eq-decl nil sets nil)
    (setof type-eq-decl nil defined_types nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number nonempty-type-decl nil numbers nil)
    (T2 formal-type-decl nil finite_fubini_scaf nil)
    (T1 formal-type-decl nil finite_fubini_scaf nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (simple? const-decl "bool" measure_space nil)
    (measurable_function nonempty-type-eq-decl nil measure_space_def
     nil)
    (measurable_function? const-decl "bool" measure_space_def nil)
    (measurable_y_section formula-decl nil finite_fubini_scaf nil)
    (mu_fin? const-decl "bool" measure_props nil)
    (subset_is_partial_order name-judgement "(partial_order?[set[T]])"
     sets_lemmas_aux nil)
    (subset_is_partial_order name-judgement "(partial_order?[set[T]])"
     sets_lemmas nil)
    (subset? const-decl "bool" sets nil)
    (TRUE const-decl "bool" booleans nil)
    (member const-decl "bool" sets nil)
    (fullset const-decl "set" sets nil)
    (image const-decl "set[R]" function_image nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (is_finite const-decl "bool" finite_sets nil)
    (set type-eq-decl nil sets nil)
    (finite_subset formula-decl nil finite_sets nil)
    (measurable_fullset name-judgement "measurable_set[T, S]"
     finite_fubini_scaf nil)
    (subset_algebra_fullset name-judgement "(S)" finite_fubini_scaf
     nil)
    (measurable_fullset name-judgement "measurable_set[T, S]"
     finite_fubini_scaf nil)
    (subset_algebra_fullset name-judgement "(S)" finite_fubini_scaf
     nil))
   shostak))
 (integral_phi1_TCC1 0
  (integral_phi1_TCC1-1 nil 3458818643
   ("" (skosimp)
    ((""
      (lemma "isf_x_section"
       ("i" "phi[[T1, T2], sigma_times(S1, S2)](E!1)" "x" "x!1"))
      (("1" (propax) nil nil)
       ("2" (rewrite "isf_phi")
        (("2" (expand "mu_fin?")
          (("2" (expand "product_measure")
            (("2" (expand "to_measure")
              (("2" (expand "measurable_set?") (("2" (propax) nil nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((phi const-decl "nat" measure_space nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (set type-eq-decl nil sets nil)
    (isf nonempty-type-eq-decl nil isf nil)
    (isf? const-decl "bool" isf nil)
    (nu formal-const-decl "finite_measure[T2, S2]" finite_fubini_scaf
     nil)
    (mu formal-const-decl "finite_measure[T1, S1]" finite_fubini_scaf
     nil)
    (fm_times const-decl
     "finite_measure[[T1, T2], sigma_times(S1, S2)]"
     product_finite_measure nil)
    (to_measure const-decl "measure_type" generalized_measure_def nil)
    (measure_type nonempty-type-eq-decl nil generalized_measure_def
     nil)
    (measure? const-decl "bool" generalized_measure_def nil)
    (extended_nnreal nonempty-type-eq-decl nil extended_nnreal
     "extended_nnreal/")
    (finite_measure nonempty-type-eq-decl nil generalized_measure_def
     nil)
    (finite_measure? const-decl "bool" generalized_measure_def nil)
    (nnreal type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (S2 formal-const-decl "sigma_algebra[T2]" finite_fubini_scaf nil)
    (S1 formal-const-decl "sigma_algebra[T1]" finite_fubini_scaf nil)
    (sigma_times const-decl "sigma_algebra[[T1, T2]]" product_sigma_def
     nil)
    (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
    (sigma_algebra? const-decl "bool" subset_algebra_def nil)
    (setofsets type-eq-decl nil sets nil)
    (setof type-eq-decl nil defined_types nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (T2 formal-type-decl nil finite_fubini_scaf nil)
    (T1 formal-type-decl nil finite_fubini_scaf nil)
    (isf_x_section formula-decl nil finite_fubini_scaf nil)
    (phi_is_simple application-judgement "simple" finite_fubini_scaf
     nil)
    (isf_phi judgement-tcc nil isf nil)
    (measurable_set? const-decl "bool" measure_space_def nil)
    (measurable_set nonempty-type-eq-decl nil measure_space_def nil)
    (mu_fin? const-decl "bool" measure_props nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil))
   nil))
 (integral_phi1_TCC2 0
  (integral_phi1_TCC2-1 nil 3458818643
   ("" (skosimp)
    (("" (expand "x_section")
      ((""
        (lemma "x_section_measurable"
         ("Z" "E!1" "x" "x1!1" "S1" "S1" "S2" "S2"))
        (("" (expand "member") (("" (propax) nil nil)) nil)) nil))
      nil))
    nil)
   ((x_section const-decl "[T1 -> set[T2]]" cross_product "topology/")
    (member const-decl "bool" sets nil)
    (x_section_measurable formula-decl nil product_sigma_def 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)
    (sigma_algebra? const-decl "bool" subset_algebra_def nil)
    (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
    (S1 formal-const-decl "sigma_algebra[T1]" finite_fubini_scaf nil)
    (S2 formal-const-decl "sigma_algebra[T2]" finite_fubini_scaf nil)
    (set type-eq-decl nil sets nil)
    (sigma_times const-decl "sigma_algebra[[T1, T2]]" product_sigma_def
     nil)
    (T1 formal-type-decl nil finite_fubini_scaf nil)
    (T2 formal-type-decl nil finite_fubini_scaf nil))
   nil))
 (integral_phi1 0
  (integral_phi1-1 nil 3458818650
   ("" (skosimp)
    (("" (apply-extensionality :hide? t)
      (("1" (expand "x_section")
        (("1" (expand "o ")
          (("1"
            (lemma "isf_integral_phi[T2, S2, to_measure(nu)]"
             ("E" "x_section(E!1, x!1)"))
            (("1" (expand "mu")
              (("1" (expand "to_measure")
                (("1" (expand "x_section" -1 1)
                  (("1" (expand "phi")
                    (("1" (expand "member") (("1" (propax) nil nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil)
             ("2" (expand "mu_fin?")
              (("2" (expand "to_measure")
                (("2" (expand "measurable_set?")
                  (("2"
                    (lemma "x_section_measurable"
                     ("Z" "E!1" "x" "x!1" "S1" "S1" "S2" "S2"))
                    (("2" (expand "member") (("2" (propax) nil nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (skosimp)
        (("2"
          (lemma "isf_phi[T2, S2, to_measure(nu)]"
           ("E" "x_section(E!1)(x!1)"))
          (("1" (expand "x_section")
            (("1" (expand "x_section")
              (("1" (expand "phi")
                (("1" (expand "member") (("1" (propax) nil nil)) nil))
                nil))
              nil))
            nil)
           ("2" (expand "mu_fin?")
            (("2" (expand "to_measure")
              (("2" (hide 2)
                (("2"
                  (lemma "x_section_measurable"
                   ("Z" "E!1" "x" "x!1" "S1" "S1" "S2" "S2"))
                  (("2" (expand "member")
                    (("2" (expand "measurable_set?")
                      (("2" (expand "x_section" 1)
                        (("2" (propax) nil nil)) nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((T1 formal-type-decl nil finite_fubini_scaf 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)
    (x_section const-decl "[T1 -> set[T2]]" cross_product "topology/")
    (O const-decl "T3" function_props nil)
    (isf_integral const-decl "real" isf nil)
    (isf nonempty-type-eq-decl nil isf nil)
    (T2 formal-type-decl nil finite_fubini_scaf nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (setof type-eq-decl nil defined_types nil)
    (setofsets type-eq-decl nil sets nil)
    (sigma_algebra? const-decl "bool" subset_algebra_def nil)
    (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
    (S2 formal-const-decl "sigma_algebra[T2]" finite_fubini_scaf nil)
    (>= const-decl "bool" reals nil)
    (nnreal type-eq-decl nil real_types nil)
    (finite_measure? const-decl "bool" generalized_measure_def nil)
    (finite_measure nonempty-type-eq-decl nil generalized_measure_def
     nil)
    (extended_nnreal nonempty-type-eq-decl nil extended_nnreal
     "extended_nnreal/")
    (measure? const-decl "bool" generalized_measure_def nil)
    (measure_type nonempty-type-eq-decl nil generalized_measure_def
     nil)
    (to_measure const-decl "measure_type" generalized_measure_def nil)
    (nu formal-const-decl "finite_measure[T2, S2]" finite_fubini_scaf
     nil)
    (isf? const-decl "bool" isf nil) (set type-eq-decl nil sets nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (sigma_times const-decl "sigma_algebra[[T1, T2]]" product_sigma_def
     nil)
    (S1 formal-const-decl "sigma_algebra[T1]" finite_fubini_scaf nil)
    (phi const-decl "nat" measure_space nil)
    (E!1 skolem-const-decl "(sigma_times(S1, S2))" finite_fubini_scaf
     nil)
    (x_section_measurable formula-decl nil product_sigma_def nil)
    (mu const-decl "nnreal" measure_props nil)
    (member const-decl "bool" sets nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (x_section const-decl "set[T2]" cross_product "topology/")
    (mu_fin? const-decl "bool" measure_props nil)
    (measurable_set nonempty-type-eq-decl nil measure_space_def nil)
    (measurable_set? const-decl "bool" measure_space_def nil)
    (isf_integral_phi formula-decl nil isf nil)
    (isf_phi judgement-tcc nil isf nil))
   shostak))
 (integral_phi2_TCC1 0
  (integral_phi2_TCC1-1 nil 3458819223
   ("" (skosimp)
    ((""
      (lemma "isf_y_section"
       ("i" "phi[[T1, T2], sigma_times(S1, S2)](E!1)" "y" "y!1"))
      (("1" (propax) nil nil)
       ("2" (hide 2)
        (("2" (rewrite "isf_phi")
          (("2" (expand "mu_fin?")
            (("2" (expand "product_measure")
              (("2" (expand "to_measure")
                (("2" (expand "measurable_set?")
                  (("2" (propax) nil nil)) nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((phi const-decl "nat" measure_space nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (set type-eq-decl nil sets nil)
    (isf nonempty-type-eq-decl nil isf nil)
    (isf? const-decl "bool" isf nil)
    (nu formal-const-decl "finite_measure[T2, S2]" finite_fubini_scaf
     nil)
    (mu formal-const-decl "finite_measure[T1, S1]" finite_fubini_scaf
     nil)
    (fm_times const-decl
     "finite_measure[[T1, T2], sigma_times(S1, S2)]"
     product_finite_measure nil)
    (to_measure const-decl "measure_type" generalized_measure_def nil)
    (measure_type nonempty-type-eq-decl nil generalized_measure_def
     nil)
    (measure? const-decl "bool" generalized_measure_def nil)
    (extended_nnreal nonempty-type-eq-decl nil extended_nnreal
     "extended_nnreal/")
    (finite_measure nonempty-type-eq-decl nil generalized_measure_def
     nil)
    (finite_measure? const-decl "bool" generalized_measure_def nil)
    (nnreal type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (S2 formal-const-decl "sigma_algebra[T2]" finite_fubini_scaf nil)
    (S1 formal-const-decl "sigma_algebra[T1]" finite_fubini_scaf nil)
    (sigma_times const-decl "sigma_algebra[[T1, T2]]" product_sigma_def
     nil)
    (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
    (sigma_algebra? const-decl "bool" subset_algebra_def nil)
    (setofsets type-eq-decl nil sets nil)
    (setof type-eq-decl nil defined_types nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (T2 formal-type-decl nil finite_fubini_scaf nil)
    (T1 formal-type-decl nil finite_fubini_scaf nil)
    (isf_y_section formula-decl nil finite_fubini_scaf nil)
    (phi_is_simple application-judgement "simple" finite_fubini_scaf
     nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (mu_fin? const-decl "bool" measure_props nil)
    (measurable_set nonempty-type-eq-decl nil measure_space_def nil)
    (measurable_set? const-decl "bool" measure_space_def nil)
    (isf_phi judgement-tcc nil isf nil))
   nil))
 (integral_phi2_TCC2 0
  (integral_phi2_TCC2-1 nil 3458819223
   ("" (skosimp)
    (("" (expand "y_section")
      ((""
        (lemma "y_section_measurable"
         ("Z" "E!1" "y" "x1!1" "S1" "S1" "S2" "S2"))
        (("" (expand "member") (("" (propax) nil nil)) nil)) nil))
      nil))
    nil)
   ((y_section const-decl "[T2 -> set[T1]]" cross_product "topology/")
    (member const-decl "bool" sets nil)
    (y_section_measurable formula-decl nil product_sigma_def 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)
    (sigma_algebra? const-decl "bool" subset_algebra_def nil)
    (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
    (S1 formal-const-decl "sigma_algebra[T1]" finite_fubini_scaf nil)
    (S2 formal-const-decl "sigma_algebra[T2]" finite_fubini_scaf nil)
    (set type-eq-decl nil sets nil)
    (sigma_times const-decl "sigma_algebra[[T1, T2]]" product_sigma_def
     nil)
    (T1 formal-type-decl nil finite_fubini_scaf nil)
    (T2 formal-type-decl nil finite_fubini_scaf nil))
   nil))
 (integral_phi2 0
  (integral_phi2-1 nil 3458819232
   ("" (skosimp)
    (("" (apply-extensionality :hide? t)
      (("1" (expand "o")
        (("1" (expand "y_section")
          (("1"
            (lemma "isf_integral_phi[T1, S1, to_measure(mu)]"
             ("E" "y_section(E!1, x!1)"))
            (("1" (expand "y_section" -1 1)
              (("1" (expand "phi")
                (("1" (expand "member")
                  (("1" (assert)
                    (("1" (expand "mu" -1)
                      (("1" (expand "to_measure")
                        (("1" (propax) nil nil)) nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil)
             ("2" (expand "mu_fin?")
              (("2" (expand "to_measure")
                (("2" (hide 2)
                  (("2"
                    (lemma "y_section_measurable"
                     ("Z" "E!1" "y" "x!1" "S1" "S1" "S2" "S2"))
                    (("2" (expand "member")
                      (("2" (expand "measurable_set?")
                        (("2" (propax) nil nil)) nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (skosimp)
        (("2"
          (lemma "isf_y_section"
           ("y" "y!1" "i" "phi[[T1, T2], sigma_times(S1, S2)](E!1)"))
          (("1" (propax) nil nil)
           ("2" (rewrite "isf_phi")
            (("2" (expand "mu_fin?")
              (("2" (expand "product_measure")
                (("2" (expand "to_measure")
                  (("2" (expand "measurable_set?")
                    (("2" (propax) nil nil)) nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((T2 formal-type-decl nil finite_fubini_scaf 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)
    (y_section const-decl "[T2 -> set[T1]]" cross_product "topology/")
    (O const-decl "T3" function_props nil)
    (isf_integral const-decl "real" isf nil)
    (isf nonempty-type-eq-decl nil isf nil)
    (T1 formal-type-decl nil finite_fubini_scaf nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (setof type-eq-decl nil defined_types nil)
    (setofsets type-eq-decl nil sets nil)
    (sigma_algebra? const-decl "bool" subset_algebra_def nil)
    (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
    (S1 formal-const-decl "sigma_algebra[T1]" finite_fubini_scaf nil)
    (>= const-decl "bool" reals nil)
    (nnreal type-eq-decl nil real_types nil)
    (finite_measure? const-decl "bool" generalized_measure_def nil)
    (finite_measure nonempty-type-eq-decl nil generalized_measure_def
     nil)
    (extended_nnreal nonempty-type-eq-decl nil extended_nnreal
     "extended_nnreal/")
    (measure? const-decl "bool" generalized_measure_def nil)
    (measure_type nonempty-type-eq-decl nil generalized_measure_def
     nil)
    (to_measure const-decl "measure_type" generalized_measure_def nil)
    (mu formal-const-decl "finite_measure[T1, S1]" finite_fubini_scaf
     nil)
    (isf? const-decl "bool" isf nil) (set type-eq-decl nil sets nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (sigma_times const-decl "sigma_algebra[[T1, T2]]" product_sigma_def
     nil)
    (S2 formal-const-decl "sigma_algebra[T2]" finite_fubini_scaf nil)
    (phi const-decl "nat" measure_space nil)
    (E!1 skolem-const-decl "(sigma_times(S1, S2))" finite_fubini_scaf
     nil)
    (y_section_measurable formula-decl nil product_sigma_def nil)
    (member const-decl "bool" sets nil)
    (mu const-decl "nnreal" measure_props nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (y_section const-decl "set[T1]" cross_product "topology/")
    (mu_fin? const-decl "bool" measure_props nil)
    (measurable_set nonempty-type-eq-decl nil measure_space_def nil)
    (measurable_set? const-decl "bool" measure_space_def nil)
    (isf_integral_phi formula-decl nil isf nil)
    (phi_is_simple application-judgement "simple" finite_fubini_scaf
     nil)
    (isf_y_section formula-decl nil finite_fubini_scaf nil)
    (fm_times const-decl
     "finite_measure[[T1, T2], sigma_times(S1, S2)]"
     product_finite_measure nil)
    (nu formal-const-decl "finite_measure[T2, S2]" finite_fubini_scaf
     nil)
    (isf_phi judgement-tcc nil isf nil))
   shostak))
 (integral_phi3_TCC1 0
  (integral_phi3_TCC1-1 nil 3458889572 ("" (subtype-tcc) nil nil)
   ((integral const-decl "real" integral nil)
    (S2 formal-const-decl "sigma_algebra[T2]" finite_fubini_scaf nil)
    (S1 formal-const-decl "sigma_algebra[T1]" finite_fubini_scaf nil)
    (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
    (sigma_algebra? const-decl "bool" subset_algebra_def nil)
    (setofsets type-eq-decl nil sets nil)
    (setof type-eq-decl nil defined_types nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T2 formal-type-decl nil finite_fubini_scaf nil)
    (T1 formal-type-decl nil finite_fubini_scaf nil)
    (fm_times const-decl
     "finite_measure[[T1, T2], sigma_times(S1, S2)]"
     product_finite_measure nil)
    (to_measure const-decl "measure_type" generalized_measure_def nil)
    (mu_fin? const-decl "bool" measure_props nil)
    (isf? const-decl "bool" isf nil)
    (phi_is_simple application-judgement "simple" finite_fubini_scaf
     nil)
    (real_minus_real_is_real application-judgement "real" reals nil))
   nil))
 (integral_phi3_TCC2 0
  (integral_phi3_TCC2-1 nil 3458889572
   ("" (skosimp)
    (("" (lemma "integral_phi1" ("E" "E!1"))
      (("" (replace -1) (("" (rewrite "x_section_integrable") nil nil))
        nil))
      nil))
    nil)
   ((S2 formal-const-decl "sigma_algebra[T2]" finite_fubini_scaf nil)
    (S1 formal-const-decl "sigma_algebra[T1]" finite_fubini_scaf nil)
    (sigma_times const-decl "sigma_algebra[[T1, T2]]" product_sigma_def
     nil)
    (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
    (sigma_algebra? const-decl "bool" subset_algebra_def nil)
    (setofsets type-eq-decl nil sets nil)
    (setof type-eq-decl nil defined_types nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T2 formal-type-decl nil finite_fubini_scaf nil)
    (T1 formal-type-decl nil finite_fubini_scaf nil)
    (integral_phi1 formula-decl nil finite_fubini_scaf nil)
    (x_section_integrable formula-decl nil product_finite_measure nil)
    (number nonempty-type-decl nil numbers 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)
    (>= const-decl "bool" reals nil)
    (nnreal type-eq-decl nil real_types nil)
    (finite_measure? const-decl "bool" generalized_measure_def nil)
    (finite_measure nonempty-type-eq-decl nil generalized_measure_def
     nil)
    (mu formal-const-decl "finite_measure[T1, S1]" finite_fubini_scaf
     nil)
    (nu formal-const-decl "finite_measure[T2, S2]" finite_fubini_scaf
     nil))
   nil))
 (integral_phi3 0
  (integral_phi3-1 nil 3458889984
   ("" (skosimp)
    (("" (rewrite "isf_integral_phi")
      (("1" (expand "mu")
        (("1" (expand "product_measure")
          (("1" (expand "to_measure")
            (("1" (expand "fm_times")
              (("1" (rewrite "integral_phi1") nil nil)) nil))
            nil))
          nil))
        nil)
       ("2" (expand "mu_fin?")
        (("2" (expand "product_measure")
          (("2" (expand "to_measure")
            (("2" (typepred "E!1")
              (("2" (expand "measurable_set?") (("2" (propax) nil nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((AND const-decl "[bool, bool -> bool]" booleans nil)
    (isf_integral_phi formula-decl nil isf nil)
    (set type-eq-decl nil sets nil)
    (measurable_set? const-decl "bool" measure_space_def nil)
    (measurable_set nonempty-type-eq-decl nil measure_space_def nil)
    (mu_fin? const-decl "bool" measure_props nil)
    (T1 formal-type-decl nil finite_fubini_scaf nil)
    (T2 formal-type-decl nil finite_fubini_scaf 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)
    (sigma_algebra? const-decl "bool" subset_algebra_def nil)
    (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
    (sigma_times const-decl "sigma_algebra[[T1, T2]]" product_sigma_def
     nil)
    (S1 formal-const-decl "sigma_algebra[T1]" finite_fubini_scaf nil)
    (S2 formal-const-decl "sigma_algebra[T2]" finite_fubini_scaf nil)
    (number nonempty-type-decl nil numbers 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)
    (>= const-decl "bool" reals nil)
    (nnreal type-eq-decl nil real_types nil)
    (finite_measure? const-decl "bool" generalized_measure_def nil)
    (finite_measure nonempty-type-eq-decl nil generalized_measure_def
     nil)
    (extended_nnreal nonempty-type-eq-decl nil extended_nnreal
     "extended_nnreal/")
    (measure? const-decl "bool" generalized_measure_def nil)
    (measure_type nonempty-type-eq-decl nil generalized_measure_def
     nil)
    (to_measure const-decl "measure_type" generalized_measure_def nil)
    (fm_times const-decl
     "finite_measure[[T1, T2], sigma_times(S1, S2)]"
     product_finite_measure nil)
    (mu formal-const-decl "finite_measure[T1, S1]" finite_fubini_scaf
     nil)
    (nu formal-const-decl "finite_measure[T2, S2]" finite_fubini_scaf
     nil)
    (phi_is_simple application-judgement "simple" finite_fubini_scaf
     nil)
    (integral_phi1 formula-decl nil finite_fubini_scaf nil)
    (mu const-decl "nnreal" measure_props nil)
    (NOT const-decl "[bool -> bool]" booleans nil))
   shostak))
 (integral_phi4_TCC1 0
  (integral_phi4_TCC1-1 nil 3458889572
   ("" (skosimp)
    (("" (rewrite "integral_phi2")
      (("" (rewrite "y_section_integrable") nil nil)) nil))
    nil)
   ((integral_phi2 formula-decl nil finite_fubini_scaf nil)
    (T1 formal-type-decl nil finite_fubini_scaf nil)
    (T2 formal-type-decl nil finite_fubini_scaf 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)
    (sigma_algebra? const-decl "bool" subset_algebra_def nil)
    (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
    (sigma_times const-decl "sigma_algebra[[T1, T2]]" product_sigma_def
     nil)
    (S1 formal-const-decl "sigma_algebra[T1]" finite_fubini_scaf nil)
    (S2 formal-const-decl "sigma_algebra[T2]" finite_fubini_scaf nil)
    (nu formal-const-decl "finite_measure[T2, S2]" finite_fubini_scaf
     nil)
    (mu formal-const-decl "finite_measure[T1, S1]" finite_fubini_scaf
     nil)
    (finite_measure nonempty-type-eq-decl nil generalized_measure_def
     nil)
    (finite_measure? const-decl "bool" generalized_measure_def nil)
    (nnreal type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number nonempty-type-decl nil numbers nil)
    (y_section_integrable formula-decl nil product_finite_measure nil))
   nil))
 (integral_phi4 0
  (integral_phi4-1 nil 3458890113
   ("" (skosimp)
    (("" (rewrite "isf_integral_phi")
      (("1" (expand "mu")
        (("1" (expand "product_measure")
          (("1" (expand "to_measure")
            (("1" (rewrite "finite_product_alt")
              (("1" (rewrite "integral_phi2") nil nil)) nil))
            nil))
          nil))
        nil)
       ("2" (expand "mu_fin?")
        (("2" (expand "measurable_set?")
          (("2" (expand "product_measure")
            (("2" (expand "to_measure") (("2" (propax) nil nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((AND const-decl "[bool, bool -> bool]" booleans nil)
    (isf_integral_phi formula-decl nil isf nil)
    (set type-eq-decl nil sets nil)
    (measurable_set? const-decl "bool" measure_space_def nil)
    (measurable_set nonempty-type-eq-decl nil measure_space_def nil)
    (mu_fin? const-decl "bool" measure_props nil)
    (T1 formal-type-decl nil finite_fubini_scaf nil)
    (T2 formal-type-decl nil finite_fubini_scaf 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)
    (sigma_algebra? const-decl "bool" subset_algebra_def nil)
    (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
    (sigma_times const-decl "sigma_algebra[[T1, T2]]" product_sigma_def
     nil)
    (S1 formal-const-decl "sigma_algebra[T1]" finite_fubini_scaf nil)
    (S2 formal-const-decl "sigma_algebra[T2]" finite_fubini_scaf nil)
    (number nonempty-type-decl nil numbers 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)
    (>= const-decl "bool" reals nil)
    (nnreal type-eq-decl nil real_types nil)
    (finite_measure? const-decl "bool" generalized_measure_def nil)
    (finite_measure nonempty-type-eq-decl nil generalized_measure_def
     nil)
    (extended_nnreal nonempty-type-eq-decl nil extended_nnreal
     "extended_nnreal/")
    (measure? const-decl "bool" generalized_measure_def nil)
    (measure_type nonempty-type-eq-decl nil generalized_measure_def
     nil)
    (to_measure const-decl "measure_type" generalized_measure_def nil)
    (fm_times const-decl
     "finite_measure[[T1, T2], sigma_times(S1, S2)]"
     product_finite_measure nil)
    (mu formal-const-decl "finite_measure[T1, S1]" finite_fubini_scaf
     nil)
    (nu formal-const-decl "finite_measure[T2, S2]" finite_fubini_scaf
     nil)
    (phi_is_simple application-judgement "simple" finite_fubini_scaf
     nil)
    (integral_phi2 formula-decl nil finite_fubini_scaf nil)
    (finite_product_alt formula-decl nil product_finite_measure nil)
    (mu const-decl "nnreal" measure_props nil))
   shostak))
 (isf_integral_x_TCC1 0
  (isf_integral_x_TCC1-1 nil 3458807583
   ("" (skosimp)
    (("" (lemma "isf_x_section" ("x" "x!1" "i" "i!1"))
      (("" (propax) nil nil)) nil))
    nil)
   ((isf nonempty-type-eq-decl nil isf nil)
    (isf? const-decl "bool" isf nil)
    (nu formal-const-decl "finite_measure[T2, S2]" finite_fubini_scaf
     nil)
    (mu formal-const-decl "finite_measure[T1, S1]" finite_fubini_scaf
     nil)
    (fm_times const-decl
     "finite_measure[[T1, T2], sigma_times(S1, S2)]"
     product_finite_measure nil)
    (to_measure const-decl "measure_type" generalized_measure_def nil)
    (measure_type nonempty-type-eq-decl nil generalized_measure_def
     nil)
    (measure? const-decl "bool" generalized_measure_def nil)
    (extended_nnreal nonempty-type-eq-decl nil extended_nnreal
     "extended_nnreal/")
    (finite_measure nonempty-type-eq-decl nil generalized_measure_def
     nil)
    (finite_measure? const-decl "bool" generalized_measure_def nil)
    (nnreal type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (S2 formal-const-decl "sigma_algebra[T2]" finite_fubini_scaf nil)
    (S1 formal-const-decl "sigma_algebra[T1]" finite_fubini_scaf nil)
    (sigma_times const-decl "sigma_algebra[[T1, T2]]" product_sigma_def
     nil)
    (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
    (sigma_algebra? const-decl "bool" subset_algebra_def nil)
    (setofsets type-eq-decl nil sets nil)
    (setof type-eq-decl nil defined_types nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (T2 formal-type-decl nil finite_fubini_scaf nil)
    (T1 formal-type-decl nil finite_fubini_scaf nil)
    (isf_x_section formula-decl nil finite_fubini_scaf nil))
   nil))
 (isf_integral_x 0
  (isf_integral_x-1 nil 3458808015
   ("" (skosimp)
    ((""
      (lemma
       "isf_induction[[T1, T2], sigma_times(S1, S2), to_measure(fm_times(mu,nu))]"
       ("P"
        "lambda i: integrable?(LAMBDA x: isf_integral(LAMBDA y: i(x, y)))"))
      (("1" (inst - "i!1")
        (("1" (assert)
          (("1" (hide 2)
            (("1" (split)
              (("1" (rewrite "isf_integral_zero")
                (("1" (rewrite "integrable_zero") nil nil)) nil)
               ("2" (skosimp)
                (("2"
                  (case-replace "(LAMBDA x:
                    isf_integral(LAMBDA y: (c!1 * phi(E!1) + i!2)(x, y)))=+[T1](*[T1](c!1,LAMBDA x:
                    isf_integral(LAMBDA y: phi(E!1)(x, y))),LAMBDA x: isf_integral(LAMBDA y: i!2(x, y)))")
                  (("1" (hide -1)
                    (("1" (rewrite "integrable_add")
                      (("1" (skosimp)
                        (("1" (rewrite "isf_x_section") nil nil)) nil)
                       ("2" (rewrite "integrable_scal")
                        (("1" (rewrite "integral_phi1")
                          (("1" (rewrite "x_section_integrable")
                            (("1" (typepred "E!1")
                              (("1"
                                (expand "measurable_set?")
                                (("1" (propax) nil nil))
                                nil))
                              nil))
                            nil)
                           ("2" (typepred "E!1")
                            (("2" (expand "measurable_set?")
                              (("2" (propax) nil nil)) nil))
                            nil))
                          nil)
                         ("2" (skosimp)
                          (("2" (rewrite "isf_x_section") nil nil))
                          nil))
                        nil)
                       ("3" (skosimp)
                        (("3" (rewrite "isf_x_section") nil nil)) nil))
                      nil))
                    nil)
                   ("2" (hide 2)
                    (("2" (apply-extensionality :hide? t)
                      (("1"
                        (lemma
                         "isf_phi[[T1,T2],sigma_times(S1,S2),to_measure(fm_times(mu,nu))]"
                         ("E" "E!1"))
                        (("1"
                          (lemma
                           "isf_scal[[T1,T2],sigma_times(S1,S2),to_measure(fm_times(mu,nu))]"
                           ("c" "c!1" "i"
                            "phi[[T1, T2], sigma_times(S1, S2)](E!1)"))
                          (("1" (typepred "i!2")
                            (("1" (expand "+" 1)
                              (("1"
                                (expand "*" 1)
                                (("1"
                                  (assert)
                                  (("1"
                                    (lemma
                                     "isf_integral_add[T2,S2,to_measure(nu)]"
                                     ("i1"
                                      "LAMBDA y: i!2(x!1, y)"
                                      "i2"
                                      "LAMBDA y:c!1 * phi(E!1)(x!1, y)"))
                                    (("1"
                                      (expand "+" -1 1)
                                      (("1"
                                        (replace -1)
                                        (("1"
                                          (hide -1)
                                          (("1"
                                            (assert)
                                            (("1"
                                              (rewrite
                                               "isf_integral_scal"
                                               1
                                               :dir
                                               rl)
                                              (("1"
                                                (expand "*")
                                                (("1"
                                                  (propax)
                                                  nil
                                                  nil))
                                                nil)
                                               ("2"
                                                (rewrite
                                                 "isf_x_section"
                                                 1)
                                                nil
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil)
                                     ("2"
                                      (lemma
                                       "isf_x_section"
                                       ("i"
                                        "(*[[T1, T2]](c!1, phi[[T1, T2], sigma_times(S1, S2)](E!1)))"
                                        "x"
                                        "x!1"))
                                      (("2"
                                        (expand "*")
                                        (("2" (propax) nil nil))
                                        nil))
                                      nil)
                                     ("3"
                                      (rewrite "isf_x_section" 1)
                                      nil
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil)
                       ("2" (skosimp)
                        (("2" (rewrite "isf_x_section") nil nil)) nil)
                       ("3" (skosimp)
                        (("3" (rewrite "isf_x_section") nil nil)) nil)
                       ("4" (skosimp)
                        (("4" (rewrite "isf_x_section") nil nil)) nil))
                      nil))
                    nil)
                   ("3" (skosimp)
                    (("3" (rewrite "isf_x_section") nil nil)) nil)
                   ("4" (skosimp)
                    (("4" (rewrite "isf_x_section") nil nil)) nil)
                   ("5" (skosimp)
                    (("5" (rewrite "isf_x_section") nil nil)) nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (skosimp) (("2" (rewrite "isf_x_section") nil nil)) nil))
      nil))
    nil)
   ((nu formal-const-decl "finite_measure[T2, S2]" finite_fubini_scaf
     nil)
    (mu formal-const-decl "finite_measure[T1, S1]" finite_fubini_scaf
     nil)
    (fm_times const-decl
     "finite_measure[[T1, T2], sigma_times(S1, S2)]"
     product_finite_measure nil)
    (to_measure const-decl "measure_type" generalized_measure_def nil)
    (measure_type nonempty-type-eq-decl nil generalized_measure_def
     nil)
    (measure? const-decl "bool" generalized_measure_def nil)
    (extended_nnreal nonempty-type-eq-decl nil extended_nnreal
     "extended_nnreal/")
    (finite_measure nonempty-type-eq-decl nil generalized_measure_def
     nil)
    (finite_measure? const-decl "bool" generalized_measure_def nil)
    (nnreal type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number nonempty-type-decl nil numbers nil)
    (S2 formal-const-decl "sigma_algebra[T2]" finite_fubini_scaf nil)
    (S1 formal-const-decl "sigma_algebra[T1]" finite_fubini_scaf nil)
    (sigma_times const-decl "sigma_algebra[[T1, T2]]" product_sigma_def
     nil)
    (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
    (sigma_algebra? const-decl "bool" subset_algebra_def nil)
    (setofsets type-eq-decl nil sets nil)
    (setof type-eq-decl nil defined_types nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T2 formal-type-decl nil finite_fubini_scaf nil)
    (T1 formal-type-decl nil finite_fubini_scaf nil)
    (isf_integral const-decl "real" isf nil)
    (integrable? const-decl "bool" integral nil)
    (pred type-eq-decl nil defined_types nil)
    (isf nonempty-type-eq-decl nil isf nil)
    (isf? const-decl "bool" isf nil)
    (isf_induction formula-decl nil isf nil)
    (isf_add application-judgement "isf" finite_fubini_scaf nil)
    (integrable_add application-judgement "integrable"
     finite_fubini_scaf nil)
    (simple_add application-judgement "simple" finite_fubini_scaf nil)
    (integrable_zero formula-decl nil integral nil)
    (isf_integral_zero formula-decl nil isf nil)
    (isf_phi application-judgement "isf" finite_fubini_scaf nil)
    (simple_scal application-judgement "simple" finite_fubini_scaf nil)
    (integrable_scal application-judgement "integrable"
     finite_fubini_scaf nil)
    (isf_scal application-judgement "isf" finite_fubini_scaf nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (+ const-decl "[T -> real]" real_fun_ops "reals/")
    (* const-decl "[T -> real]" real_fun_ops "reals/")
    (set type-eq-decl nil sets nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (phi const-decl "nat" measure_space nil)
    (measurable_set? const-decl "bool" measure_space_def nil)
    (measurable_set nonempty-type-eq-decl nil measure_space_def nil)
    (mu_fin? const-decl "bool" measure_props nil)
    (integrable nonempty-type-eq-decl nil integral nil)
    (integrable_add judgement-tcc nil integral nil)
    (isf_x_section formula-decl nil finite_fubini_scaf nil)
    (integral_phi1 formula-decl nil finite_fubini_scaf nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (x_section_integrable formula-decl nil product_finite_measure nil)
    (integrable_scal judgement-tcc nil integral nil)
    (i!2 skolem-const-decl
     "isf[[T1, T2], sigma_times(S1, S2), to_measure(fm_times(mu, nu))]"
     finite_fubini_scaf nil)
    (E!1 skolem-const-decl "(mu_fin?)" finite_fubini_scaf nil)
    (c!1 skolem-const-decl "real" finite_fubini_scaf nil)
    (isf_scal judgement-tcc nil isf nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (isf_integral_scal formula-decl nil isf nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (isf_integral_add formula-decl nil isf nil)
    (isf_phi judgement-tcc nil isf nil))
   shostak))
 (isf_integral_y_TCC1 0
  (isf_integral_y_TCC1-1 nil 3458807583
   ("" (skosimp)
    (("" (lemma "isf_y_section" ("y" "y!1" "i" "i!1"))
      (("" (propax) nil nil)) nil))
    nil)
   ((isf nonempty-type-eq-decl nil isf nil)
    (isf? const-decl "bool" isf nil)
    (nu formal-const-decl "finite_measure[T2, S2]" finite_fubini_scaf
     nil)
    (mu formal-const-decl "finite_measure[T1, S1]" finite_fubini_scaf
     nil)
    (fm_times const-decl
     "finite_measure[[T1, T2], sigma_times(S1, S2)]"
     product_finite_measure nil)
    (to_measure const-decl "measure_type" generalized_measure_def nil)
    (measure_type nonempty-type-eq-decl nil generalized_measure_def
     nil)
    (measure? const-decl "bool" generalized_measure_def nil)
    (extended_nnreal nonempty-type-eq-decl nil extended_nnreal
     "extended_nnreal/")
    (finite_measure nonempty-type-eq-decl nil generalized_measure_def
     nil)
    (finite_measure? const-decl "bool" generalized_measure_def nil)
    (nnreal type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (S2 formal-const-decl "sigma_algebra[T2]" finite_fubini_scaf nil)
    (S1 formal-const-decl "sigma_algebra[T1]" finite_fubini_scaf nil)
    (sigma_times const-decl "sigma_algebra[[T1, T2]]" product_sigma_def
     nil)
    (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
    (sigma_algebra? const-decl "bool" subset_algebra_def nil)
    (setofsets type-eq-decl nil sets nil)
    (setof type-eq-decl nil defined_types nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (T2 formal-type-decl nil finite_fubini_scaf nil)
    (T1 formal-type-decl nil finite_fubini_scaf nil)
    (isf_y_section formula-decl nil finite_fubini_scaf nil))
   nil))
 (isf_integral_y 0
  (isf_integral_y-1 nil 3458816919
   ("" (skosimp)
    ((""
      (lemma
       "isf_induction[[T1, T2], sigma_times(S1, S2), to_measure(fm_times(mu,nu))]"
       ("P"
        "lambda i: integrable?(LAMBDA y: isf_integral(LAMBDA x: i(x, y)))"))
      (("1" (inst - "i!1")
        (("1" (assert)
          (("1" (hide 2)
            (("1" (rewrite "isf_integral_zero")
              (("1" (rewrite "integrable_zero")
                (("1" (skosimp)
                  (("1"
                    (case "forall y: isf?(phi(lambda x: E!1(x,y)))")
                    (("1" (expand "+" 1)
                      (("1" (expand "*" 1)
                        (("1"
                          (case "forall y: isf_integral(LAMBDA x:
                                   i!2(x, y) + c!1 * phi(E!1)(x, y)) = isf_integral(LAMBDA x: i!2(x, y))+c!1*isf_integral(phi(LAMBDA x: E!1(x, y)))")
                          (("1" (rewrite "extensionality_postulate" -1)
                            (("1" (replace -1)
                              (("1"
                                (hide -1)
                                (("1"
                                  (lemma
                                   "integrable_add"
                                   ("f1"
                                    "LAMBDA (y):
                    isf_integral(LAMBDA x: i!2(x, y))"
                                    "f2"
                                    "lambda y: c!1 * isf_integral(phi(LAMBDA x: E!1(x, y)))"))
                                  (("1"
                                    (expand "+" -1)
                                    (("1" (propax) nil nil))
                                    nil)
                                   ("2"
                                    (hide 2)
                                    (("2"
                                      (hide -2)
                                      (("2"
                                        (lemma
                                         "integrable_scal[T2, S2, to_measure(nu)]"
                                         ("c"
                                          "c!1"
                                          "f"
                                          "lambda y: isf_integral[T1, S1, to_measure(mu)]
                  (phi[T1, S1](LAMBDA x: E!1(x, y)))"))
                                        (("1"
                                          (expand "*" -1)
                                          (("1" (propax) nil nil))
                                          nil)
                                         ("2"
                                          (hide 2)
                                          (("2"
                                            (lemma
                                             "integral_phi2"
                                             ("E" "E!1"))
                                            (("1"
                                              (expand "phi")
                                              (("1"
                                                (expand "member")
                                                (("1"
                                                  (replace -1)
                                                  (("1"
                                                    (hide -1)
                                                    (("1"
                                                      (lemma
                                                       "y_section_integrable"
                                                       ("mu"
                                                        "mu"
                                                        "M"
                                                        "E!1"
                                                        "nu"
                                                        "nu"))
                                                      (("1"
                                                        (propax)
                                                        nil
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil)
                                             ("2"
                                              (typepred "E!1")
                                              (("2"
                                                (expand
                                                 "measurable_set?")
                                                (("2"
                                                  (propax)
                                                  nil
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil)
                                   ("3" (propax) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil)
                           ("2" (skosimp)
                            (("2" (inst - "y!1")
                              (("2"
                                (hide 2 -2)
                                (("2"
                                  (lemma
                                   "isf_integral_scal"
                                   ("c"
                                    "c!1"
                                    "i"
                                    "phi(LAMBDA x: E!1(x, y!1))"))
                                  (("2"
                                    (replace -1 1 rl)
                                    (("2"
                                      (rewrite
                                       "isf_integral_add"
                                       1
                                       :dir
                                       rl)
                                      (("1"
                                        (expand "*")
                                        (("1"
                                          (expand
                                           "+
")
                                          (("1"
                                            (expand "phi")
                                            (("1"
                                              (expand "member")
                                              (("1" (propax) nil nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil)
                                       ("2"
                                        (rewrite "isf_y_section")
                                        nil
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil)
                           ("3" (propax) nil nil)
                           ("4" (skosimp)
                            (("4" (rewrite "isf_y_section") nil nil))
                            nil)
                           ("5" (skosimp)
                            (("5" (inst - "y!1")
                              (("5"
                                (lemma
                                 "isf_scal"
                                 ("c"
                                  "c!1"
                                  "i"
                                  "phi(LAMBDA x: E!1(x, y!1))"))
                                (("1"
                                  (lemma
                                   "isf_add"
                                   ("i1"
                                    "LAMBDA x:
             i!2(x, y!1)"
                                    "i2"
                                    "*[T1](c!1, phi(LAMBDA x: E!1(x, y!1)))"))
                                  (("1"
                                    (hide 2)
                                    (("1"
                                      (expand "+")
                                      (("1"
                                        (expand "*")
                                        (("1"
                                          (expand "phi")
                                          (("1"
                                            (expand "member")
                                            (("1" (propax) nil nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil)
                                   ("2" (propax) nil nil)
                                   ("3"
                                    (rewrite "isf_y_section")
                                    nil
                                    nil))
                                  nil)
                                 ("2" (propax) nil nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil)
                     ("2" (hide -1 2)
                      (("2" (skosimp)
                        (("2" (rewrite "isf_phi")
                          (("2" (typepred "E!1")
                            (("2" (expand "mu_fin?")
                              (("2"
                                (expand "to_measure")
                                (("2"
                                  (expand "measurable_set?")
                                  (("2"
                                    (hide -2 2)
                                    (("2"
                                      (lemma
                                       "y_section_measurable"
                                       ("Z"
                                        "E!1"
                                        "y"
                                        "y!1"
                                        "S1"
                                        "S1"
                                        "S2"
                                        "S2"))
                                      (("2"
                                        (expand "member")
                                        (("2"
                                          (expand "y_section")
                                          (("2" (assert) nil nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (hide 2)
        (("2" (skosimp) (("2" (rewrite "isf_y_section") nil nil)) nil))
        nil))
      nil))
    nil)
   ((nu formal-const-decl "finite_measure[T2, S2]" finite_fubini_scaf
     nil)
    (mu formal-const-decl "finite_measure[T1, S1]" finite_fubini_scaf
     nil)
    (fm_times const-decl
     "finite_measure[[T1, T2], sigma_times(S1, S2)]"
     product_finite_measure nil)
    (to_measure const-decl "measure_type" generalized_measure_def nil)
    (measure_type nonempty-type-eq-decl nil generalized_measure_def
     nil)
    (measure? const-decl "bool" generalized_measure_def nil)
    (extended_nnreal nonempty-type-eq-decl nil extended_nnreal
     "extended_nnreal/")
    (finite_measure nonempty-type-eq-decl nil generalized_measure_def
     nil)
    (finite_measure? const-decl "bool" generalized_measure_def nil)
    (nnreal type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number nonempty-type-decl nil numbers nil)
    (S2 formal-const-decl "sigma_algebra[T2]" finite_fubini_scaf nil)
    (S1 formal-const-decl "sigma_algebra[T1]" finite_fubini_scaf nil)
    (sigma_times const-decl "sigma_algebra[[T1, T2]]" product_sigma_def
     nil)
    (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
    (sigma_algebra? const-decl "bool" subset_algebra_def nil)
    (setofsets type-eq-decl nil sets nil)
    (setof type-eq-decl nil defined_types nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T2 formal-type-decl nil finite_fubini_scaf nil)
    (T1 formal-type-decl nil finite_fubini_scaf nil)
    (isf_integral const-decl "real" isf nil)
    (integrable? const-decl "bool" integral nil)
    (pred type-eq-decl nil defined_types nil)
    (isf nonempty-type-eq-decl nil isf nil)
    (isf? const-decl "bool" isf nil)
    (isf_induction formula-decl nil isf nil)
    (isf_add application-judgement "isf" finite_fubini_scaf nil)
    (integrable_add application-judgement "integrable"
     finite_fubini_scaf nil)
    (simple_add application-judgement "simple" finite_fubini_scaf nil)
    (isf_integral_zero formula-decl nil isf nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (isf_phi judgement-tcc nil isf nil)
    (y_section_measurable formula-decl nil product_sigma_def nil)
    (y_section const-decl "set[T1]" cross_product "topology/")
    (+ const-decl "[T -> real]" real_fun_ops "reals/")
    (real_plus_real_is_real application-judgement "real" reals nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (integrable_add judgement-tcc nil integral nil)
    (integrable nonempty-type-eq-decl nil integral nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (y_section_integrable formula-decl nil product_finite_measure nil)
    (member const-decl "bool" sets nil)
    (integral_phi2 formula-decl nil finite_fubini_scaf nil)
    (integrable_scal judgement-tcc nil integral nil)
    (extensionality_postulate formula-decl nil functions nil)
    (isf_integral_scal formula-decl nil isf nil)
    (isf_integral_add formula-decl nil isf nil)
    (isf_y_section formula-decl nil finite_fubini_scaf nil)
    (isf_add judgement-tcc nil isf nil)
    (isf_scal judgement-tcc nil isf nil)
    (* const-decl "[T -> real]" real_fun_ops "reals/")
    (set type-eq-decl nil sets nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (phi const-decl "nat" measure_space nil)
    (measurable_set? const-decl "bool" measure_space_def nil)
    (measurable_set nonempty-type-eq-decl nil measure_space_def nil)
    (mu_fin? const-decl "bool" measure_props nil)
    (integrable_zero formula-decl nil integral nil))
   shostak))
 (isf_fubini_tonelli_3_TCC1 0
  (isf_fubini_tonelli_3_TCC1-1 nil 3458807583
   ("" (skosimp)
    (("" (lemma "isf_integral_x" ("i" "i!1")) (("" (propax) nil nil))
      nil))
    nil)
   ((isf nonempty-type-eq-decl nil isf nil)
    (isf? const-decl "bool" isf nil)
    (nu formal-const-decl "finite_measure[T2, S2]" finite_fubini_scaf
     nil)
    (mu formal-const-decl "finite_measure[T1, S1]" finite_fubini_scaf
     nil)
    (fm_times const-decl
     "finite_measure[[T1, T2], sigma_times(S1, S2)]"
     product_finite_measure nil)
    (to_measure const-decl "measure_type" generalized_measure_def nil)
    (measure_type nonempty-type-eq-decl nil generalized_measure_def
     nil)
    (measure? const-decl "bool" generalized_measure_def nil)
    (extended_nnreal nonempty-type-eq-decl nil extended_nnreal
     "extended_nnreal/")
    (finite_measure nonempty-type-eq-decl nil generalized_measure_def
     nil)
    (finite_measure? const-decl "bool" generalized_measure_def nil)
    (nnreal type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (S2 formal-const-decl "sigma_algebra[T2]" finite_fubini_scaf nil)
    (S1 formal-const-decl "sigma_algebra[T1]" finite_fubini_scaf nil)
    (sigma_times const-decl "sigma_algebra[[T1, T2]]" product_sigma_def
     nil)
    (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
    (sigma_algebra? const-decl "bool" subset_algebra_def nil)
    (setofsets type-eq-decl nil sets nil)
    (setof type-eq-decl nil defined_types nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (T2 formal-type-decl nil finite_fubini_scaf nil)
    (T1 formal-type-decl nil finite_fubini_scaf nil)
    (isf_integral_x formula-decl nil finite_fubini_scaf nil))
   nil))
 (isf_fubini_tonelli_3 0
  (isf_fubini_tonelli_3-1 nil 3458817775
   ("" (skosimp)
    ((""
      (lemma
       "isf_induction[[T1,T2],sigma_times(S1,S2),to_measure(fm_times(mu,nu))]"
       ("i1" "i!1" "P"
        "lambda (i: isf[[T1, T2], sigma_times(S1, S2), to_measure(fm_times(mu,nu))]):
        isf_integral(i) =
         integral(LAMBDA x: isf_integral(LAMBDA y: i(x, y)))"))
      (("1" (assert)
        (("1" (hide 2)
          (("1" (split)
            (("1" (rewrite "isf_integral_zero")
              (("1" (rewrite "isf_integral_zero")
                (("1" (rewrite "integral_zero") nil nil)) nil))
              nil)
             ("2" (skosimp)
              (("2" (typepred "E!1")
                (("2" (lemma "isf_phi" ("E" "E!1"))
                  (("2" (lemma "isf_scal" ("c" "c!1" "i" "phi(E!1)"))
                    (("2"
                      (lemma "isf_add"
                       ("i1" "*[[T1, T2]](c!1, phi(E!1))" "i2" "i!2"))
                      (("2" (rewrite "isf_integral_add" 1)
                        (("2" (rewrite "isf_integral_scal" 1)
                          (("2" (rewrite "integral_phi3")
                            (("1" (replace -6)
                              (("1"
                                (hide -6)
                                (("1"
                                  (rewrite "integral_scal" 1 :dir rl)
                                  (("1"
                                    (rewrite "integral_add" 1 :dir rl)
                                    (("1"
                                      (expand "*" 1 1)
                                      (("1"
                                        (expand "+" 1 1)
                                        (("1"
                                          (case-replace
                                           "(LAMBDA (x_1: T1):
                 isf_integral(LAMBDA y: i!2(x_1, y)) +
                  c!1 * isf_integral(LAMBDA y: phi(E!1)(x_1, y)))=(LAMBDA x:
                  isf_integral(LAMBDA y: (+[[T1,T2]]((*[[T1, T2]](c!1, phi(E!1))),i!2)(x, y))))")
                                          (("1"
                                            (hide 2)
                                            (("1"
                                              (apply-extensionality
                                               :hide?
                                               t)
                                              (("1"
                                                (rewrite
                                                 "isf_integral_scal"
                                                 1
                                                 :dir
                                                 rl)
                                                (("1"
                                                  (lemma
                                                   "isf_integral_add[T2,S2,to_measure(nu)]"
                                                   ("i1"
                                                    "*[T2](c!1,LAMBDA y: phi(E!1)(x!1, y))"
                                                    "i2"
                                                    "LAMBDA y: i!2(x!1, y)"))
                                                  (("1"
                                                    (replace -1 1 rl)
                                                    (("1"
                                                      (expand "*")
                                                      (("1"
                                                        (expand "+")
                                                        (("1"
                                                          (propax)
                                                          nil
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil)
                                                   ("2"
                                                    (rewrite
                                                     "isf_x_section")
                                                    nil
                                                    nil))
                                                  nil)
                                                 ("2"
                                                  (rewrite
                                                   "isf_x_section")
                                                  nil
                                                  nil))
                                                nil)
                                               ("2"
                                                (skosimp)
                                                (("2"
                                                  (rewrite
                                                   "isf_x_section")
                                                  nil
                                                  nil))
                                                nil)
                                               ("3"
                                                (skosimp)
                                                (("3"
                                                  (rewrite
                                                   "isf_x_section")
                                                  nil
                                                  nil))
                                                nil)
                                               ("4"
                                                (skosimp)
                                                (("4"
                                                  (rewrite
                                                   "isf_x_section")
                                                  nil
                                                  nil))
                                                nil))
                                              nil))
                                            nil)
                                           ("2"
                                            (skosimp)
                                            (("2"
                                              (rewrite "isf_x_section")
                                              nil
                                              nil))
                                            nil)
                                           ("3"
                                            (skosimp)
                                            (("3"
                                              (rewrite "isf_x_section")
                                              nil
                                              nil))
                                            nil)
                                           ("4"
                                            (skosimp)
                                            (("4"
                                              (rewrite "isf_x_section")
                                              nil
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil)
                                     ("2"
                                      (rewrite "isf_integral_x")
                                      nil
                                      nil)
                                     ("3"
                                      (skosimp)
                                      (("3"
                                        (rewrite "isf_x_section")
                                        nil
                                        nil))
                                      nil)
                                     ("4"
                                      (skosimp)
                                      (("4"
                                        (rewrite "isf_x_section")
                                        nil
                                        nil))
                                      nil))
                                    nil)
                                   ("2"
                                    (rewrite "isf_integral_x")
                                    (("2"
                                      (expand "phi")
                                      (("2" (propax) nil nil))
                                      nil))
                                    nil)
                                   ("3"
                                    (skosimp)
                                    (("3"
                                      (rewrite "isf_x_section")
                                      nil
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil)
                             ("2" (expand "measurable_set?")
                              (("2" (propax) nil nil)) nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (hide 2)
        (("2" (skosimp) (("2" (rewrite "isf_integral_x") nil nil))
          nil))
        nil)
       ("3" (skosimp) (("3" (rewrite "isf_x_section") nil nil)) nil))
      nil))
    nil)
   ((nu formal-const-decl "finite_measure[T2, S2]" finite_fubini_scaf
     nil)
    (mu formal-const-decl "finite_measure[T1, S1]" finite_fubini_scaf
     nil)
    (fm_times const-decl
     "finite_measure[[T1, T2], sigma_times(S1, S2)]"
     product_finite_measure nil)
    (to_measure const-decl "measure_type" generalized_measure_def nil)
    (measure_type nonempty-type-eq-decl nil generalized_measure_def
     nil)
    (measure? const-decl "bool" generalized_measure_def nil)
    (extended_nnreal nonempty-type-eq-decl nil extended_nnreal
     "extended_nnreal/")
    (finite_measure nonempty-type-eq-decl nil generalized_measure_def
     nil)
    (finite_measure? const-decl "bool" generalized_measure_def nil)
    (nnreal type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number nonempty-type-decl nil numbers nil)
    (S2 formal-const-decl "sigma_algebra[T2]" finite_fubini_scaf nil)
    (S1 formal-const-decl "sigma_algebra[T1]" finite_fubini_scaf nil)
    (sigma_times const-decl "sigma_algebra[[T1, T2]]" product_sigma_def
     nil)
    (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
    (sigma_algebra? const-decl "bool" subset_algebra_def nil)
    (setofsets type-eq-decl nil sets nil)
    (setof type-eq-decl nil defined_types nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T2 formal-type-decl nil finite_fubini_scaf nil)
    (T1 formal-type-decl nil finite_fubini_scaf nil)
    (integral const-decl "real" integral nil)
    (integrable nonempty-type-eq-decl nil integral nil)
    (integrable? const-decl "bool" integral nil)
    (isf_integral const-decl "real" isf nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (pred type-eq-decl nil defined_types nil)
    (isf nonempty-type-eq-decl nil isf nil)
    (isf? const-decl "bool" isf nil)
    (isf_induction formula-decl nil isf nil)
    (isf_phi judgement-tcc nil isf nil)
    (simple_scal application-judgement "simple" finite_fubini_scaf nil)
    (integrable_scal application-judgement "integrable"
     finite_fubini_scaf nil)
    (isf_scal application-judgement "isf" finite_fubini_scaf nil)
    (isf_add judgement-tcc nil isf nil)
    (* const-decl "[T -> real]" real_fun_ops "reals/")
    (isf_integral_scal formula-decl nil isf nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (integral_scal formula-decl nil integral nil)
    (isf_integral_x formula-decl nil finite_fubini_scaf nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (c!1 skolem-const-decl "real" finite_fubini_scaf nil)
    (E!1 skolem-const-decl "(mu_fin?)" finite_fubini_scaf nil)
    (i!2 skolem-const-decl
     "isf[[T1, T2], sigma_times(S1, S2), to_measure(fm_times(mu, nu))]"
     finite_fubini_scaf nil)
    (isf_x_section formula-decl nil finite_fubini_scaf nil)
    (+ const-decl "[T -> real]" real_fun_ops "reals/")
    (integral_add formula-decl nil integral nil)
    (integral_phi3 formula-decl nil finite_fubini_scaf nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (isf_integral_add formula-decl nil isf nil)
    (phi const-decl "nat" measure_space nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (isf_scal judgement-tcc nil isf nil)
    (isf_phi application-judgement "isf" finite_fubini_scaf nil)
    (mu_fin? const-decl "bool" measure_props nil)
    (measurable_set nonempty-type-eq-decl nil measure_space_def nil)
    (measurable_set? const-decl "bool" measure_space_def nil)
    (set type-eq-decl nil sets nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (isf_integral_zero formula-decl nil isf nil)
    (integral_zero formula-decl nil integral nil)
    (simple_add application-judgement "simple" finite_fubini_scaf nil)
    (integrable_add application-judgement "integrable"
     finite_fubini_scaf nil)
    (isf_add application-judgement "isf" finite_fubini_scaf nil))
   shostak))
 (isf_fubini_tonelli_4_TCC1 0
  (isf_fubini_tonelli_4_TCC1-1 nil 3458807583
   ("" (skosimp)
    (("" (lemma "isf_integral_y" ("i" "i!1")) (("" (propax) nil nil))
      nil))
    nil)
   ((isf nonempty-type-eq-decl nil isf nil)
    (isf? const-decl "bool" isf nil)
    (nu formal-const-decl "finite_measure[T2, S2]" finite_fubini_scaf
     nil)
    (mu formal-const-decl "finite_measure[T1, S1]" finite_fubini_scaf
     nil)
    (fm_times const-decl
     "finite_measure[[T1, T2], sigma_times(S1, S2)]"
     product_finite_measure nil)
    (to_measure const-decl "measure_type" generalized_measure_def nil)
    (measure_type nonempty-type-eq-decl nil generalized_measure_def
     nil)
    (measure? const-decl "bool" generalized_measure_def nil)
    (extended_nnreal nonempty-type-eq-decl nil extended_nnreal
     "extended_nnreal/")
    (finite_measure nonempty-type-eq-decl nil generalized_measure_def
     nil)
    (finite_measure? const-decl "bool" generalized_measure_def nil)
    (nnreal type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (S2 formal-const-decl "sigma_algebra[T2]" finite_fubini_scaf nil)
    (S1 formal-const-decl "sigma_algebra[T1]" finite_fubini_scaf nil)
    (sigma_times const-decl "sigma_algebra[[T1, T2]]" product_sigma_def
     nil)
    (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
    (sigma_algebra? const-decl "bool" subset_algebra_def nil)
    (setofsets type-eq-decl nil sets nil)
    (setof type-eq-decl nil defined_types nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (T2 formal-type-decl nil finite_fubini_scaf nil)
    (T1 formal-type-decl nil finite_fubini_scaf nil)
    (isf_integral_y formula-decl nil finite_fubini_scaf nil))
   nil))
 (isf_fubini_tonelli_4 0
  (isf_fubini_tonelli_4-1 nil 3459238687
   ("" (skosimp)
    ((""
      (lemma
       "isf_induction[[T1,T2],sigma_times(S1,S2),to_measure(fm_times(mu,nu))]"
       ("i1" "i!1" "P"
        "lambda (i: isf[[T1, T2], sigma_times(S1, S2), to_measure(fm_times(mu,nu))]):
        isf_integral(i) =
         integral(LAMBDA y: isf_integral(LAMBDA x: i(x, y)))"))
      (("1" (assert)
        (("1" (hide 2)
          (("1" (split)
            (("1" (rewrite "isf_integral_zero")
              (("1" (rewrite "isf_integral_zero")
                (("1" (rewrite "integral_zero") nil nil)) nil))
              nil)
             ("2" (skosimp*)
              (("2" (typepred "E!1")
                (("2" (lemma "isf_phi" ("E" "E!1"))
                  (("2" (lemma "isf_scal" ("c" "c!1" "i" "phi(E!1)"))
                    (("2"
                      (lemma "isf_add"
                       ("i1" "*[[T1, T2]](c!1, phi(E!1))" "i2" "i!2"))
                      (("2" (rewrite "isf_integral_add" 1)
                        (("2" (rewrite "isf_integral_scal" 1)
                          (("2" (rewrite "integral_phi4")
                            (("1" (replace -6)
                              (("1"
                                (rewrite "integral_scal" 1 :dir rl)
                                (("1"
                                  (rewrite "integral_add" 1 :dir rl)
                                  (("1"
                                    (expand "*" 1 1)
                                    (("1"
                                      (expand "+" 1 1)
                                      (("1"
                                        (case-replace
                                         "(LAMBDA y:
                 isf_integral(LAMBDA x: i!2(x, y)) +
                  c!1 * isf_integral(LAMBDA x: phi(E!1)(x, y)))=(LAMBDA y:
                  isf_integral(LAMBDA x: (c!1 * phi(E!1) + i!2)(x, y)))")
                                        (("1"
                                          (hide 2)
                                          (("1"
                                            (apply-extensionality
                                             :hide?
                                             t)
                                            (("1"
                                              (rewrite
                                               "isf_integral_scal"
                                               1
                                               :dir
                                               rl)
                                              (("1"
                                                (rewrite
                                                 "isf_integral_add"
                                                 1
                                                 :dir
                                                 rl)
                                                (("1"
                                                  (expand "*")
                                                  (("1"
                                                    (expand "+")
                                                    (("1"
                                                      (propax)
                                                      nil
                                                      nil))
                                                    nil))
                                                  nil)
                                                 ("2"
                                                  (rewrite
                                                   "isf_y_section")
                                                  nil
                                                  nil))
                                                nil)
                                               ("2"
                                                (rewrite
                                                 "isf_y_section")
                                                nil
                                                nil))
                                              nil)
                                             ("2"
                                              (skosimp)
                                              (("2"
                                                (expand "+")
                                                (("2"
                                                  (expand "*")
                                                  (("2"
                                                    (expand "phi")
                                                    (("2"
                                                      (expand "member")
                                                      (("2"
                                                        (lemma
                                                         "isf_y_section"
                                                         ("i"
                                                          "LAMBDA (x: [T1, T2]):
             i!2(x) + c!1 * IF E!1(x) THEN 1 ELSE 0 ENDIF"
                                                          "y"
                                                          "y!1"))
                                                        (("1"
                                                          (assert)
                                                          nil
                                                          nil)
                                                         ("2"
                                                          (propax)
                                                          nil
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil)
                                             ("3"
                                              (skosimp)
                                              (("3"
                                                (rewrite
                                                 "isf_y_section")
                                                nil
                                                nil))
                                              nil)
                                             ("4"
                                              (skosimp)
                                              (("4"
                                                (rewrite
                                                 "isf_y_section")
                                                nil
                                                nil))
                                              nil))
                                            nil))
                                          nil)
                                         ("2"
                                          (skosimp)
                                          (("2"
                                            (hide 2)
                                            (("2"
                                              (rewrite "isf_y_section")
                                              nil
                                              nil))
                                            nil))
                                          nil)
                                         ("3"
                                          (skosimp)
                                          (("3"
                                            (rewrite "isf_y_section")
                                            nil
                                            nil))
                                          nil)
                                         ("4"
                                          (skosimp)
                                          (("4"
                                            (rewrite "isf_y_section")
                                            nil
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil)
                                   ("2"
                                    (hide 2)
                                    (("2"
                                      (rewrite "isf_integral_y")
                                      nil
                                      nil))
                                    nil)
                                   ("3"
                                    (skosimp)
                                    (("3"
                                      (rewrite "isf_y_section")
                                      nil
                                      nil))
                                    nil)
                                   ("4"
                                    (skosimp)
                                    (("4"
                                      (rewrite "isf_y_section")
                                      nil
                                      nil))
                                    nil))
                                  nil)
                                 ("2"
                                  (hide 2)
                                  (("2"
                                    (rewrite "isf_integral_y")
                                    (("2"
                                      (hide 2)
                                      (("2"
                                        (expand "phi")
                                        (("2" (propax) nil nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil)
                                 ("3"
                                  (skosimp)
                                  (("3"
                                    (rewrite "isf_y_section")
                                    nil
                                    nil))
                                  nil))
                                nil))
                              nil)
                             ("2" (expand "measurable_set?")
                              (("2" (propax) nil nil)) nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (skosimp) (("2" (rewrite "isf_integral_y") nil nil)) nil)
       ("3" (skosimp) (("3" (rewrite "isf_y_section") nil nil)) nil))
      nil))
    nil)
   ((nu formal-const-decl "finite_measure[T2, S2]" finite_fubini_scaf
     nil)
    (mu formal-const-decl "finite_measure[T1, S1]" finite_fubini_scaf
     nil)
    (fm_times const-decl
     "finite_measure[[T1, T2], sigma_times(S1, S2)]"
     product_finite_measure nil)
    (to_measure const-decl "measure_type" generalized_measure_def nil)
    (measure_type nonempty-type-eq-decl nil generalized_measure_def
     nil)
    (measure? const-decl "bool" generalized_measure_def nil)
    (extended_nnreal nonempty-type-eq-decl nil extended_nnreal
     "extended_nnreal/")
    (finite_measure nonempty-type-eq-decl nil generalized_measure_def
     nil)
    (finite_measure? const-decl "bool" generalized_measure_def nil)
    (nnreal type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number nonempty-type-decl nil numbers nil)
    (S2 formal-const-decl "sigma_algebra[T2]" finite_fubini_scaf nil)
    (S1 formal-const-decl "sigma_algebra[T1]" finite_fubini_scaf nil)
    (sigma_times const-decl "sigma_algebra[[T1, T2]]" product_sigma_def
     nil)
    (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
    (sigma_algebra? const-decl "bool" subset_algebra_def nil)
    (setofsets type-eq-decl nil sets nil)
    (setof type-eq-decl nil defined_types nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T2 formal-type-decl nil finite_fubini_scaf nil)
    (T1 formal-type-decl nil finite_fubini_scaf nil)
    (integral const-decl "real" integral nil)
    (integrable nonempty-type-eq-decl nil integral nil)
    (integrable? const-decl "bool" integral nil)
    (isf_integral const-decl "real" isf nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (pred type-eq-decl nil defined_types nil)
    (isf nonempty-type-eq-decl nil isf nil)
    (isf? const-decl "bool" isf nil)
    (isf_induction formula-decl nil isf nil)
    (isf_phi judgement-tcc nil isf nil)
    (simple_scal application-judgement "simple" finite_fubini_scaf nil)
    (integrable_scal application-judgement "integrable"
     finite_fubini_scaf nil)
    (isf_scal application-judgement "isf" finite_fubini_scaf nil)
    (isf_add judgement-tcc nil isf nil)
    (* const-decl "[T -> real]" real_fun_ops "reals/")
    (isf_integral_scal formula-decl nil isf nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (integral_add formula-decl nil integral nil)
    (+ const-decl "[T -> real]" real_fun_ops "reals/")
    (member const-decl "bool" sets nil)
    (IF const-decl "[boolean, T, T -> T]" if_def nil)
    (isf_y_section formula-decl nil finite_fubini_scaf nil)
    (i!2 skolem-const-decl
     "isf[[T1, T2], sigma_times(S1, S2), to_measure(fm_times(mu, nu))]"
     finite_fubini_scaf nil)
    (E!1 skolem-const-decl "(mu_fin?)" finite_fubini_scaf nil)
    (c!1 skolem-const-decl "real" finite_fubini_scaf nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (isf_integral_y formula-decl nil finite_fubini_scaf nil)
    (integral_scal formula-decl nil integral nil)
    (integral_phi4 formula-decl nil finite_fubini_scaf nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (isf_integral_add formula-decl nil isf nil)
    (phi const-decl "nat" measure_space nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (isf_scal judgement-tcc nil isf nil)
    (isf_phi application-judgement "isf" finite_fubini_scaf nil)
    (mu_fin? const-decl "bool" measure_props nil)
    (measurable_set nonempty-type-eq-decl nil measure_space_def nil)
    (measurable_set? const-decl "bool" measure_space_def nil)
    (set type-eq-decl nil sets nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (isf_integral_zero formula-decl nil isf nil)
    (integral_zero formula-decl nil integral nil)
    (simple_add application-judgement "simple" finite_fubini_scaf nil)
    (integrable_add application-judgement "integrable"
     finite_fubini_scaf nil)
    (isf_add application-judgement "isf" finite_fubini_scaf nil))
   shostak)))