(card_comp_transitive
 (card_lt_transitive 0
  (card_lt_transitive-1 nil 3316960965
   ("" (expand "card_lt")
    (("" (lemma "injective_dichotomous")
      (("" (prop)
        (("" (skosimp*)
          (("" (use "composition_injective[T3, T1, T2]")
            (("" (inst? 2) nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((T2 formal-type-decl nil card_comp_transitive nil)
    (T1 formal-type-decl nil card_comp_transitive nil)
    (injective_dichotomous formula-decl nil set_dichotomous "orders/")
    (O const-decl "T3" function_props nil)
    (f!1 skolem-const-decl "[T1 -> T2]" card_comp_transitive nil)
    (f!2 skolem-const-decl "[T3 -> T1]" card_comp_transitive nil)
    (injective? const-decl "bool" functions nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T3 formal-type-decl nil card_comp_transitive nil)
    (composition_injective judgement-tcc nil function_props nil)
    (card_lt const-decl "bool" card_comp nil))
   shostak))
 (card_lt_le_transitive 0
  (card_lt_le_transitive-1 nil 3316961013
   ("" (expand* "card_lt" "card_le")
    (("" (skosimp*)
      (("" (use "composition_injective[T2, T3, T1]")
        (("" (inst?) nil nil)) nil))
      nil))
    nil)
   ((O const-decl "T3" function_props nil)
    (f!2 skolem-const-decl "[T3 -> T1]" card_comp_transitive nil)
    (f!1 skolem-const-decl "[T2 -> T3]" card_comp_transitive nil)
    (injective? const-decl "bool" functions nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T1 formal-type-decl nil card_comp_transitive nil)
    (T3 formal-type-decl nil card_comp_transitive nil)
    (T2 formal-type-decl nil card_comp_transitive nil)
    (composition_injective judgement-tcc nil function_props nil)
    (card_lt const-decl "bool" card_comp nil)
    (card_le const-decl "bool" card_comp nil))
   shostak))
 (card_lt_eq_transitive 0
  (card_lt_eq_transitive-1 nil 3316961037
   ("" (expand* "card_lt" "card_eq" "bijective?")
    (("" (skosimp*)
      (("" (use "composition_injective[T2, T3, T1]")
        (("" (inst?) nil nil)) nil))
      nil))
    nil)
   ((O const-decl "T3" function_props nil)
    (f!2 skolem-const-decl "[T3 -> T1]" card_comp_transitive nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (injective? const-decl "bool" functions nil)
    (f!1 skolem-const-decl "[T2 -> T3]" card_comp_transitive nil)
    (T1 formal-type-decl nil card_comp_transitive nil)
    (T3 formal-type-decl nil card_comp_transitive nil)
    (T2 formal-type-decl nil card_comp_transitive nil)
    (composition_injective judgement-tcc nil function_props nil)
    (card_lt const-decl "bool" card_comp nil)
    (bijective? const-decl "bool" functions nil)
    (card_eq const-decl "bool" card_comp nil))
   shostak))
 (card_le_lt_transitive 0
  (card_le_lt_transitive-1 nil 3316961078
   ("" (expand* "card_le" "card_lt")
    (("" (skosimp*)
      (("" (use "composition_injective[T3, T1, T2]")
        (("" (inst?) nil nil)) nil))
      nil))
    nil)
   ((O const-decl "T3" function_props nil)
    (f!1 skolem-const-decl "[T1 -> T2]" card_comp_transitive nil)
    (f!2 skolem-const-decl "[T3 -> T1]" card_comp_transitive nil)
    (injective? const-decl "bool" functions nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T2 formal-type-decl nil card_comp_transitive nil)
    (T1 formal-type-decl nil card_comp_transitive nil)
    (T3 formal-type-decl nil card_comp_transitive nil)
    (composition_injective judgement-tcc nil function_props nil)
    (card_le const-decl "bool" card_comp nil)
    (card_lt const-decl "bool" card_comp nil))
   shostak))
 (card_eq_lt_transitive 0
  (card_eq_lt_transitive-1 nil 3316961096
   ("" (expand* "card_eq" "card_lt" "bijective?")
    (("" (skosimp*)
      (("" (use "composition_injective[T3, T1, T2]")
        (("" (inst?) nil nil)) nil))
      nil))
    nil)
   ((O const-decl "T3" function_props nil)
    (f!1 skolem-const-decl "[T1 -> T2]" card_comp_transitive nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (injective? const-decl "bool" functions nil)
    (f!2 skolem-const-decl "[T3 -> T1]" card_comp_transitive nil)
    (T2 formal-type-decl nil card_comp_transitive nil)
    (T1 formal-type-decl nil card_comp_transitive nil)
    (T3 formal-type-decl nil card_comp_transitive nil)
    (composition_injective judgement-tcc nil function_props nil)
    (card_eq const-decl "bool" card_comp nil)
    (bijective? const-decl "bool" functions nil)
    (card_lt const-decl "bool" card_comp nil))
   shostak))
 (card_le_transitive 0
  (card_le_transitive-1 nil 3316961118
   ("" (expand "card_le")
    (("" (skosimp*)
      (("" (use "composition_injective[T1, T2, T3]")
        (("" (inst?) nil nil)) nil))
      nil))
    nil)
   ((O const-decl "T3" function_props nil)
    (f!2 skolem-const-decl "[T2 -> T3]" card_comp_transitive nil)
    (f!1 skolem-const-decl "[T1 -> T2]" card_comp_transitive nil)
    (injective? const-decl "bool" functions nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T3 formal-type-decl nil card_comp_transitive nil)
    (T2 formal-type-decl nil card_comp_transitive nil)
    (T1 formal-type-decl nil card_comp_transitive nil)
    (composition_injective judgement-tcc nil function_props nil)
    (card_le const-decl "bool" card_comp nil))
   shostak))
 (card_le_eq_transitive 0
  (card_le_eq_transitive-1 nil 3316961145
   ("" (expand* "card_le" "card_eq" "bijective?")
    (("" (skosimp*)
      (("" (use "composition_injective[T1, T2, T3]")
        (("" (inst?) nil nil)) nil))
      nil))
    nil)
   ((O const-decl "T3" function_props nil)
    (f!2 skolem-const-decl "[T2 -> T3]" card_comp_transitive nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (injective? const-decl "bool" functions nil)
    (f!1 skolem-const-decl "[T1 -> T2]" card_comp_transitive nil)
    (T3 formal-type-decl nil card_comp_transitive nil)
    (T2 formal-type-decl nil card_comp_transitive nil)
    (T1 formal-type-decl nil card_comp_transitive nil)
    (composition_injective judgement-tcc nil function_props nil)
    (card_le const-decl "bool" card_comp nil)
    (bijective? const-decl "bool" functions nil)
    (card_eq const-decl "bool" card_comp nil))
   shostak))
 (card_eq_le_transitive 0
  (card_eq_le_transitive-1 nil 3316961166
   ("" (expand* "card_eq" "card_le" "bijective?")
    (("" (skosimp*)
      (("" (use "composition_injective[T1, T2, T3]")
        (("" (inst?) nil nil)) nil))
      nil))
    nil)
   ((O const-decl "T3" function_props nil)
    (f!2 skolem-const-decl "[T2 -> T3]" card_comp_transitive nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (injective? const-decl "bool" functions nil)
    (f!1 skolem-const-decl "[T1 -> T2]" card_comp_transitive nil)
    (T3 formal-type-decl nil card_comp_transitive nil)
    (T2 formal-type-decl nil card_comp_transitive nil)
    (T1 formal-type-decl nil card_comp_transitive nil)
    (composition_injective judgement-tcc nil function_props nil)
    (card_eq const-decl "bool" card_comp nil)
    (bijective? const-decl "bool" functions nil)
    (card_le const-decl "bool" card_comp nil))
   shostak))
 (card_eq_transitive 0
  (card_eq_transitive-1 nil 3316961183
   ("" (expand "card_eq")
    (("" (skosimp*)
      (("" (use "composition_bijective[T1, T2, T3]")
        (("" (inst?) nil nil)) nil))
      nil))
    nil)
   ((O const-decl "T3" function_props nil)
    (f!2 skolem-const-decl "[T2 -> T3]" card_comp_transitive nil)
    (f!1 skolem-const-decl "[T1 -> T2]" card_comp_transitive nil)
    (bijective? const-decl "bool" functions nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T3 formal-type-decl nil card_comp_transitive nil)
    (T2 formal-type-decl nil card_comp_transitive nil)
    (T1 formal-type-decl nil card_comp_transitive nil)
    (composition_bijective judgement-tcc nil function_props nil)
    (card_eq const-decl "bool" card_comp nil))
   shostak))
 (card_eq_ge_transitive 0
  (card_eq_ge_transitive-1 nil 3316961212
   ("" (expand* "card_eq" "card_ge")
    (("" (skosimp*)
      (("" (use "bijective_inverse_exists[T1, T2]")
        (("" (expand "exists1")
          (("" (skosimp*)
            (("" (use "bij_inv_is_bij_alt[T1, T2]")
              (("" (expand "bijective?" -1)
                (("" (flatten)
                  (("" (use "composition_injective[T3, T2, T1]")
                    (("" (inst?) nil nil)) nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((exists1 const-decl "bool" exists1 nil)
    (bij_inv_is_bij_alt formula-decl nil function_inverse_def nil)
    (x!1 skolem-const-decl "[T2 -> T1]" card_comp_transitive nil)
    (inverse? const-decl "bool" function_inverse_def nil)
    (O const-decl "T3" function_props nil)
    (injective? const-decl "bool" functions nil)
    (f!2 skolem-const-decl "[T3 -> T2]" card_comp_transitive nil)
    (composition_injective judgement-tcc nil function_props nil)
    (T3 formal-type-decl nil card_comp_transitive nil)
    (f!1 skolem-const-decl "[T1 -> T2]" card_comp_transitive nil)
    (bijective? const-decl "bool" functions nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T2 formal-type-decl nil card_comp_transitive nil)
    (T1 formal-type-decl nil card_comp_transitive nil)
    (bijective_inverse_exists formula-decl nil function_inverse_def
     nil)
    (card_eq const-decl "bool" card_comp nil)
    (card_ge const-decl "bool" card_comp nil))
   shostak))
 (card_ge_eq_transitive 0
  (card_ge_eq_transitive-1 nil 3316961287
   ("" (expand* "card_ge" "card_eq")
    (("" (skosimp*)
      (("" (use "bijective_inverse_exists[T2, T3]")
        (("" (expand "exists1")
          (("" (skosimp*)
            (("" (use "bij_inv_is_bij_alt[T2, T3]")
              (("" (expand "bijective?" -1)
                (("" (flatten)
                  (("" (use "composition_injective[T3, T2, T1]")
                    (("" (inst?) nil nil)) nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((exists1 const-decl "bool" exists1 nil)
    (bij_inv_is_bij_alt formula-decl nil function_inverse_def nil)
    (x!1 skolem-const-decl "[T3 -> T2]" card_comp_transitive nil)
    (inverse? const-decl "bool" function_inverse_def nil)
    (O const-decl "T3" function_props nil)
    (f!1 skolem-const-decl "[T2 -> T1]" card_comp_transitive nil)
    (injective? const-decl "bool" functions nil)
    (composition_injective judgement-tcc nil function_props nil)
    (T1 formal-type-decl nil card_comp_transitive nil)
    (f!2 skolem-const-decl "[T2 -> T3]" card_comp_transitive nil)
    (bijective? const-decl "bool" functions nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T3 formal-type-decl nil card_comp_transitive nil)
    (T2 formal-type-decl nil card_comp_transitive nil)
    (bijective_inverse_exists formula-decl nil function_inverse_def
     nil)
    (card_ge const-decl "bool" card_comp nil)
    (card_eq const-decl "bool" card_comp nil))
   shostak))
 (card_ge_transitive 0
  (card_ge_transitive-1 nil 3316961349
   ("" (expand "card_ge")
    (("" (skosimp*)
      (("" (use "composition_injective[T3, T2, T1]")
        (("" (inst?) nil nil)) nil))
      nil))
    nil)
   ((O const-decl "T3" function_props nil)
    (f!1 skolem-const-decl "[T2 -> T1]" card_comp_transitive nil)
    (f!2 skolem-const-decl "[T3 -> T2]" card_comp_transitive nil)
    (injective? const-decl "bool" functions nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T1 formal-type-decl nil card_comp_transitive nil)
    (T2 formal-type-decl nil card_comp_transitive nil)
    (T3 formal-type-decl nil card_comp_transitive nil)
    (composition_injective judgement-tcc nil function_props nil)
    (card_ge const-decl "bool" card_comp nil))
   shostak))
 (card_eq_gt_transitive 0
  (card_eq_gt_transitive-1 nil 3316961376
   ("" (expand* "card_eq" "card_gt")
    (("" (skosimp*)
      (("" (use "bijective_inverse_exists[T1, T2]")
        (("" (expand "exists1")
          (("" (skosimp*)
            (("" (use "bij_inv_is_bij_alt[T1, T2]")
              (("" (expand "bijective?" -1)
                (("" (flatten)
                  (("" (use "composition_injective[T2, T1, T3]")
                    (("" (inst?) nil nil)) nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((exists1 const-decl "bool" exists1 nil)
    (bij_inv_is_bij_alt formula-decl nil function_inverse_def nil)
    (x!1 skolem-const-decl "[T2 -> T1]" card_comp_transitive nil)
    (inverse? const-decl "bool" function_inverse_def nil)
    (O const-decl "T3" function_props nil)
    (f!2 skolem-const-decl "[T1 -> T3]" card_comp_transitive nil)
    (injective? const-decl "bool" functions nil)
    (composition_injective judgement-tcc nil function_props nil)
    (T3 formal-type-decl nil card_comp_transitive nil)
    (f!1 skolem-const-decl "[T1 -> T2]" card_comp_transitive nil)
    (bijective? const-decl "bool" functions nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T2 formal-type-decl nil card_comp_transitive nil)
    (T1 formal-type-decl nil card_comp_transitive nil)
    (bijective_inverse_exists formula-decl nil function_inverse_def
     nil)
    (card_eq const-decl "bool" card_comp nil)
    (card_gt const-decl "bool" card_comp nil))
   shostak))
 (card_ge_gt_transitive 0
  (card_ge_gt_transitive-1 nil 3316961423
   ("" (expand* "card_ge" "card_gt")
    (("" (skosimp*)
      (("" (use "composition_injective[T2, T1, T3]")
        (("" (inst?) nil nil)) nil))
      nil))
    nil)
   ((O const-decl "T3" function_props nil)
    (f!2 skolem-const-decl "[T1 -> T3]" card_comp_transitive nil)
    (f!1 skolem-const-decl "[T2 -> T1]" card_comp_transitive nil)
    (injective? const-decl "bool" functions nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T3 formal-type-decl nil card_comp_transitive nil)
    (T1 formal-type-decl nil card_comp_transitive nil)
    (T2 formal-type-decl nil card_comp_transitive nil)
    (composition_injective judgement-tcc nil function_props nil)
    (card_ge const-decl "bool" card_comp nil)
    (card_gt const-decl "bool" card_comp nil))
   shostak))
 (card_gt_eq_transitive 0
  (card_gt_eq_transitive-1 nil 3316961447
   ("" (expand* "card_gt" "card_eq")
    (("" (skosimp*)
      (("" (use "bijective_inverse_exists[T2, T3]")
        (("" (expand "exists1")
          (("" (skosimp*)
            (("" (use "bij_inv_is_bij_alt[T2, T3]")
              (("" (expand "bijective?" -1)
                (("" (flatten)
                  (("" (use "composition_injective[T1, T3, T2]")
                    (("" (inst?) nil nil)) nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((exists1 const-decl "bool" exists1 nil)
    (bij_inv_is_bij_alt formula-decl nil function_inverse_def nil)
    (x!1 skolem-const-decl "[T3 -> T2]" card_comp_transitive nil)
    (inverse? const-decl "bool" function_inverse_def nil)
    (O const-decl "T3" function_props nil)
    (injective? const-decl "bool" functions nil)
    (f!2 skolem-const-decl "[T1 -> T3]" card_comp_transitive nil)
    (composition_injective judgement-tcc nil function_props nil)
    (T1 formal-type-decl nil card_comp_transitive nil)
    (f!1 skolem-const-decl "[T2 -> T3]" card_comp_transitive nil)
    (bijective? const-decl "bool" functions nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T3 formal-type-decl nil card_comp_transitive nil)
    (T2 formal-type-decl nil card_comp_transitive nil)
    (bijective_inverse_exists formula-decl nil function_inverse_def
     nil)
    (card_gt const-decl "bool" card_comp nil)
    (card_eq const-decl "bool" card_comp nil))
   shostak))
 (card_gt_ge_transitive 0
  (card_gt_ge_transitive-1 nil 3316961503
   ("" (expand* "card_gt" "card_ge")
    (("" (skosimp*)
      (("" (use "composition_injective[T1, T3, T2]")
        (("" (inst?) nil nil)) nil))
      nil))
    nil)
   ((O const-decl "T3" function_props nil)
    (f!1 skolem-const-decl "[T3 -> T2]" card_comp_transitive nil)
    (f!2 skolem-const-decl "[T1 -> T3]" card_comp_transitive nil)
    (injective? const-decl "bool" functions nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T2 formal-type-decl nil card_comp_transitive nil)
    (T3 formal-type-decl nil card_comp_transitive nil)
    (T1 formal-type-decl nil card_comp_transitive nil)
    (composition_injective judgement-tcc nil function_props nil)
    (card_gt const-decl "bool" card_comp nil)
    (card_ge const-decl "bool" card_comp nil))
   shostak))
 (card_gt_transitive 0
  (card_gt_transitive-1 nil 3316961525
   ("" (expand "card_gt")
    (("" (lemma "injective_dichotomous")
      (("" (prop)
        (("" (skosimp*)
          (("" (use "composition_injective[T2, T1, T3]")
            (("" (inst? 2) nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((T2 formal-type-decl nil card_comp_transitive nil)
    (T1 formal-type-decl nil card_comp_transitive nil)
    (injective_dichotomous formula-decl nil set_dichotomous "orders/")
    (O const-decl "T3" function_props nil)
    (f!2 skolem-const-decl "[T1 -> T3]" card_comp_transitive nil)
    (f!1 skolem-const-decl "[T2 -> T1]" card_comp_transitive nil)
    (injective? const-decl "bool" functions nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T3 formal-type-decl nil card_comp_transitive nil)
    (composition_injective judgement-tcc nil function_props nil)
    (card_gt const-decl "bool" card_comp nil))
   shostak)))