(|min_seq| (|Imin_TCC1| "" (SKOSIMP*) (("" (ASSERT) NIL)))
 (|Imin_TCC2| "" (SUBTYPE-TCC) NIL)
 (|Imin_TCC3| ""
  (INST 1 "(LAMBDA ((s: seqs), (ii: dom(s)), (jj:abv(ii, s))):
                    Imin[length(s),T,<=](seq(s),ii,jj))")
  (("" (SKOSIMP*)
    (("" (TYPEPRED "Imin[length(s!1), T, <=](seq(s!1), ii!1, jj!1)")
      (("" (INST?) (("1" (ASSERT) NIL) ("2" (ASSERT) NIL)))))))))
 (|Imin_seq_1_TCC1| "" (SUBTYPE-TCC) NIL)
 (|Imin_seq_1| "" (SKOSIMP*)
  (("" (TYPEPRED "Imin(s!1, ii!1, ii!1)")
    (("1" (INST?) (("1" (ASSERT) NIL) ("2" (ASSERT) NIL)))
     ("2" (SKOSIMP*) (("2" (ASSERT) NIL)))))))
 (|imin_TCC1| "" (INST 1 "(LAMBDA s: Imin(s,0,length(s)-1))")
  (("" (SKOSIMP*)
    (("" (TYPEPRED "Imin(s!1, 0, length(s!1) - 1)")
      (("1" (ASSERT) (("1" (SKOSIMP*) (("1" (INST?) (("1" (ASSERT) NIL)))))))
       ("2" (HIDE 2) (("2" (SKOSIMP*) (("2" (ASSERT) NIL)))))))))))
 (|min_TCC1| "" (INST 1 "(LAMBDA s: seq(s)(imin(s)))")
  (("" (SKOSIMP*)
    (("" (PROP)
      (("1" (SKOSIMP*) (("1" (TYPEPRED "imin(s!1)") (("1" (INST?) NIL)))))
       ("2" (INST?) NIL)))))))
 (|min_seq_lem| "" (SKOSIMP*) (("" (TYPEPRED "min(s!1)") (("" (INST?) NIL)))))
 (|min_seq_in?| "" (SKOSIMP*)
  (("" (EXPAND "in?")
    (("" (TYPEPRED "min(s!1)")
      (("" (SKOSIMP*)
        (("" (HIDE -1) (("" (INST?) (("" (ASSERT) NIL)))))))))))))
 (|min_seq_def| "" (SKOSIMP*)
  (("" (PROP)
    (("1" (REWRITE "min_seq_lem") NIL) ("2" (REWRITE "min_seq_in?") NIL)))))
 (|min_seq_it_is| "" (SKOSIMP*)
  (("" (TYPEPRED "min(s!1)")
    (("" (EXPAND "in?")
      (("" (SKOSIMP*)
        (("" (REPLACE -2 * RL)
          (("" (HIDE -2)
            (("" (REPLACE -3)
              (("" (HIDE -3)
                (("" (INST?)
                  (("" (INST -2 "jj!1")
                    (("" (TYPEPRED "<=")
                      (("" (EXPAND "total_order?")
                        (("" (EXPAND "partial_order?")
                          (("" (FLATTEN)
                            (("" (EXPAND "antisymmetric?")
                              (("" (INST?)
                                (("" (ASSERT)
                                  NIL)))))))))))))))))))))))))))))))))
 (|imin_seq_lem| "" (SKOSIMP*)
  (("" (TYPEPRED "imin(s!1)")
    (("" (TYPEPRED "min(s!1)")
      (("" (SKOSIMP*)
        (("" (REPLACE -2 * RL)
          (("" (HIDE -2)
            (("" (INST?)
              (("" (INST -3 "jj!1")
                (("" (TYPEPRED "min_seq.<=")
                  (("" (EXPAND "total_order?")
                    (("" (EXPAND "partial_order?")
                      (("" (FLATTEN)
                        (("" (EXPAND "antisymmetric?")
                          (("" (INST?)
                            (("" (ASSERT) NIL)))))))))))))))))))))))))))))
 (|imin_seq_1| "" (SKOSIMP*)
  (("" (TYPEPRED "imin(s!1)") (("" (ASSERT) NIL)))))
 (|min_seq_2_TCC1| "" (SUBTYPE-TCC) NIL)
 (|min_seq_2_TCC2| "" (SUBTYPE-TCC) NIL)
 (|min_seq_2| "" (SKOSIMP*)
  (("" (TYPEPRED "min(s!1)")
    (("" (SKOSIMP*)
      (("" (REPLACE -2 * RL)
        (("" (HIDE -2)
          (("" (INST-CP -1 "0")
            (("" (INST -1 "1")
              (("1" (LIFT-IF)
                (("1" (GROUND)
                  (("1" (TYPEPRED "jj!1")
                    (("1" (CASE-REPLACE "jj!1 = 0 OR jj!1 = 1")
                      (("1" (PROP)
                        (("1" (ASSERT) NIL)
                         ("2" (REPLACE -1)
                          (("2" (HIDE -1)
                            (("2" (TYPEPRED "min_seq.<=")
                              (("2" (EXPAND "total_order?")
                                (("2" (EXPAND "partial_order?")
                                  (("2" (FLATTEN)
                                    (("2" (EXPAND "antisymmetric?")
                                      (("2"
                                        (INST?)
                                        (("2" (ASSERT) NIL)))))))))))))))))))
                       ("2" (ASSERT) NIL)))))))))
               ("2" (ASSERT) NIL))))))))))))))))