(relation_extension_props
 (extended_equiv_class_non_empty 0
  (extended_equiv_class_non_empty-1 nil 3571925758
   ("" (skolem-typepred)
    (("" (expand "nonempty?")
      (("" (expand "empty?")
        (("" (expand "member")
          (("" (expand "extended_equiv_class")
            (("" (expand "rel_extension")
              (("" (inst -3 "m!1")
                (("" (prop)
                  (("1" (expand "equivalence?")
                    (("1" (prop)
                      (("1" (expand "reflexive?")
                        (("1" (inst?) nil nil)) nil))
                      nil))
                    nil)
                   ("2" (expand "equivalence?")
                    (("2" (prop)
                      (("2" (expand "reflexive?")
                        (("2" (inst? -4) nil nil)) nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((nonempty? const-decl "bool" sets nil)
    (member const-decl "bool" sets nil)
    (rel_extension const-decl "set[[[T, U], [T, U]]]"
     relation_extension nil)
    (reflexive? const-decl "bool" relations nil)
    (extended_equiv_class const-decl "set[[T, U]]" relation_extension
     nil)
    (empty? const-decl "bool" sets nil)
    (U formal-nonempty-type-decl nil relation_extension_props nil)
    (equivalence type-eq-decl nil relations nil)
    (equivalence? const-decl "bool" relations nil)
    (PRED type-eq-decl nil defined_types nil)
    (T formal-nonempty-type-decl nil relation_extension_props nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (nonempty_equivClass_impl_extended_equiv_class_non_empty 0
  (nonempty_equivClass_impl_extended_equiv_class_non_empty-1 nil
   3571925823
   ("" (skolem!)
    (("" (expand "nonempty?")
      (("" (expand "empty?")
        (("" (expand "member")
          (("" (expand "EquivClass")
            (("" (expand "extended_equiv_class")
              (("" (expand "rel_extension")
                (("" (prop)
                  (("1" (typepred "le_T!1")
                    (("1" (expand "equivalence?")
                      (("1" (prop)
                        (("1" (expand "reflexive?")
                          (("1" (inst -1 "m!1`1")
                            (("1" (typepred "le_U!1")
                              (("1"
                                (expand "equivalence?")
                                (("1"
                                  (prop)
                                  (("1"
                                    (expand "reflexive?")
                                    (("1"
                                      (inst?)
                                      (("1"
                                        (inst?)
                                        (("1"
                                          (skolem!)
                                          (("1" (prop) nil nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil)
                   ("2" (skolem!)
                    (("2" (prop) (("2" (inst?) nil nil)) nil)) nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((nonempty? const-decl "bool" sets nil)
    (member const-decl "bool" sets nil)
    (extended_equiv_class const-decl "set[[T, U]]" relation_extension
     nil)
    (reflexive? const-decl "bool" relations nil)
    (U formal-nonempty-type-decl nil relation_extension_props nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (T formal-nonempty-type-decl nil relation_extension_props nil)
    (PRED type-eq-decl nil defined_types nil)
    (equivalence? const-decl "bool" relations nil)
    (equivalence type-eq-decl nil relations nil)
    (rel_extension const-decl "set[[[T, U], [T, U]]]"
     relation_extension nil)
    (EquivClass const-decl "set[T]" QuotientDefinition nil)
    (empty? const-decl "bool" sets nil))
   shostak))
 (nonempty_equivClass_iff_extended_equiv_classT_non_empty 0
  (nonempty_equivClass_iff_extended_equiv_classT_non_empty-1 nil
   3571925865 ("" (grind) nil nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (T formal-nonempty-type-decl nil relation_extension_props nil)
    (PRED type-eq-decl nil defined_types nil)
    (equivalence? const-decl "bool" relations nil)
    (equivalence type-eq-decl nil relations nil)
    (U formal-nonempty-type-decl nil relation_extension_props nil)
    (transitive? const-decl "bool" relations nil)
    (symmetric? const-decl "bool" relations nil)
    (reflexive? const-decl "bool" relations nil)
    (EquivClass const-decl "set[T]" QuotientDefinition nil)
    (member const-decl "bool" sets nil)
    (empty? const-decl "bool" sets nil)
    (nonempty? const-decl "bool" sets nil)
    (proj_tuple_1 const-decl "[[[T, U] -> T]]" relation_extension nil)
    (rel_extension const-decl "set[[[T, U], [T, U]]]"
     relation_extension nil)
    (extended_equiv_class const-decl "set[[T, U]]" relation_extension
     nil)
    (extended_equiv_classT const-decl "set[T]" relation_extension nil))
   shostak))
 (nonempty_equivClass_iff_extended_equiv_classU_non_empty 0
  (nonempty_equivClass_iff_extended_equiv_classU_non_empty-1 nil
   3571925898 ("" (grind) nil nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (T formal-nonempty-type-decl nil relation_extension_props nil)
    (PRED type-eq-decl nil defined_types nil)
    (equivalence? const-decl "bool" relations nil)
    (equivalence type-eq-decl nil relations nil)
    (U formal-nonempty-type-decl nil relation_extension_props nil)
    (transitive? const-decl "bool" relations nil)
    (symmetric? const-decl "bool" relations nil)
    (reflexive? const-decl "bool" relations nil)
    (EquivClass const-decl "set[T]" QuotientDefinition nil)
    (member const-decl "bool" sets nil)
    (empty? const-decl "bool" sets nil)
    (nonempty? const-decl "bool" sets nil)
    (proj_tuple_2 const-decl "[[[T, U] -> U]]" relation_extension nil)
    (rel_extension const-decl "set[[[T, U], [T, U]]]"
     relation_extension nil)
    (extended_equiv_class const-decl "set[[T, U]]" relation_extension
     nil)
    (extended_equiv_classU const-decl "set[U]" relation_extension nil))
   shostak))
 (proj_tuple_1_equiv_class_representative 0
  (proj_tuple_1_equiv_class_representative-1 nil 3571925968
   ("" (skosimp*)
    (("" (expand "proj_tuple_1")
      (("" (replace -1 1 rl)
        (("" (expand "repEC")
          (("" (typepred "choose(EquivClass(le_T!1)(m!1`1))")
            (("" (expand "EquivClass") (("" (propax) nil nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((proj_tuple_1 const-decl "[[[T, U] -> T]]" relation_extension nil)
    (repEC const-decl "T" QuotientDefinition nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (T formal-nonempty-type-decl nil relation_extension_props nil)
    (set type-eq-decl nil sets nil)
    (EquivClass const-decl "set[T]" QuotientDefinition nil)
    (PRED type-eq-decl nil defined_types nil)
    (equivalence? const-decl "bool" relations nil)
    (equivalence type-eq-decl nil relations nil)
    (U formal-nonempty-type-decl nil relation_extension_props nil)
    (nonempty? const-decl "bool" sets nil)
    (choose const-decl "(p)" sets nil))
   shostak))
 (proj_tuple_2_equiv_class_representative 0
  (proj_tuple_2_equiv_class_representative-1 nil 3571925998
   ("" (skolem!)
    (("" (prop)
      (("" (expand "proj_tuple_2")
        (("" (replace -1 1 rl)
          (("" (expand "repEC")
            (("" (typepred "choose(EquivClass(le_U!1)(m!1`2))")
              (("" (expand "EquivClass") (("" (propax) nil nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((choose const-decl "(p)" sets nil)
    (nonempty? const-decl "bool" sets nil)
    (T formal-nonempty-type-decl nil relation_extension_props nil)
    (equivalence type-eq-decl nil relations nil)
    (equivalence? const-decl "bool" relations nil)
    (PRED type-eq-decl nil defined_types nil)
    (EquivClass const-decl "set[T]" QuotientDefinition nil)
    (set type-eq-decl nil sets nil)
    (U formal-nonempty-type-decl nil relation_extension_props nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (repEC const-decl "T" QuotientDefinition nil)
    (proj_tuple_2 const-decl "[[[T, U] -> U]]" relation_extension nil))
   shostak)))