(csequence_length_comp
 (length_lt_le 0
  (length_lt_le-1 nil 3513689376
   ("" (expand* "length_lt" "length_le")
    (("" (skosimp) (("" (ground) nil nil)) nil)) nil)
   ((real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (length_lt const-decl "bool" csequence_length_comp nil)
    (length_le const-decl "bool" csequence_length_comp nil))
   shostak))
 (length_gt_ge 0
  (length_gt_ge-1 nil 3513689391
   ("" (expand* "length_gt" "length_ge")
    (("" (skosimp) (("" (ground) nil nil)) nil)) nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (length_gt const-decl "bool" csequence_length_comp nil)
    (length_ge const-decl "bool" csequence_length_comp nil))
   shostak))
 (length_eq_le 0
  (length_eq_le-1 nil 3513689401
   ("" (expand* "length_eq" "length_le")
    (("" (skosimp) (("" (ground) nil nil)) nil)) nil)
   ((real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (length_eq const-decl "bool" csequence_length_comp nil)
    (length_le const-decl "bool" csequence_length_comp nil))
   shostak))
 (length_eq_ge 0
  (length_eq_ge-1 nil 3513689413
   ("" (expand* "length_eq" "length_ge")
    (("" (skosimp) (("" (ground) nil nil)) nil)) nil)
   ((real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (length_eq const-decl "bool" csequence_length_comp nil)
    (length_ge const-decl "bool" csequence_length_comp nil))
   shostak))
 (length_lt_neq 0
  (length_lt_neq-1 nil 3513689424
   ("" (expand* "length_lt" "length_eq")
    (("" (skosimp) (("" (ground) nil nil)) nil)) nil)
   ((real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (length_lt const-decl "bool" csequence_length_comp nil)
    (length_eq const-decl "bool" csequence_length_comp nil))
   shostak))
 (length_gt_neq 0
  (length_gt_neq-1 nil 3513689440
   ("" (expand* "length_gt" "length_eq")
    (("" (skosimp) (("" (ground) nil nil)) nil)) nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (length_gt const-decl "bool" csequence_length_comp nil)
    (length_eq const-decl "bool" csequence_length_comp nil))
   shostak))
 (length_eq_empty 0
  (length_eq_empty-1 nil 3513689453
   ("" (skosimp)
    (("" (expand "length_eq")
      (("" (use "length_empty?_rew[T2]")
        (("" (use "length_empty?_rew[T1]") (("" (ground) nil nil))
          nil))
        nil))
      nil))
    nil)
   ((length_eq const-decl "bool" csequence_length_comp nil)
    (T1 formal-type-decl nil csequence_length_comp nil)
    (csequence type-decl nil csequence_codt nil)
    (T2 formal-type-decl nil csequence_length_comp nil)
    (length_empty?_rew formula-decl nil csequence_length nil))
   shostak))
 (length_eq_rest 0
  (length_eq_rest-1 nil 3513689486
   ("" (expand "length_eq")
    (("" (expand "is_finite" 1 1)
      (("" (expand "is_finite" 1 2)
        (("" (expand "is_finite" 1 3)
          (("" (expand "is_finite" 1 4)
            (("" (expand "length" 1 1)
              (("" (expand "length" 1 2) (("" (propax) nil nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((is_finite inductive-decl "bool" csequence_props nil)
    (length def-decl "{n | has_length(fseq, n)}" csequence_length nil)
    (length_eq const-decl "bool" csequence_length_comp nil))
   shostak)))