DEFINITION flt_arith2()
TYPE =
       ∀c1:C
         .∀c2:C.∀t1:T.∀i:nat.(flt c1 t1 c2 (TLRef i))→∀k2:K.∀t2:T.∀j:nat.(flt c1 t1 (CHead c2 k2 t2) (TLRef j))
BODY =
        assume c1: C
        assume c2: C
        assume t1: T
        assume : nat
          we must prove (flt c1 t1 c2 (TLRef __1))→∀k2:K.∀t2:T.∀j:nat.(flt c1 t1 (CHead c2 k2 t2) (TLRef j))
          or equivalently 
                lt (plus (cweight c1) (tweight t1)) (plus (cweight c2) (S O))
                  →K→∀t2:T.nat→(flt c1 t1 (CHead c2 __3 t2) (TLRef __1))
           suppose H: lt (plus (cweight c1) (tweight t1)) (plus (cweight c2) (S O))
           assume : K
           assume t2: T
           assume : nat
             (h1) 
                by (le_plus_l . .)
le (cweight c2) (plus (cweight c2) (tweight t2))
             end of h1
             (h2) 
                by (le_n .)
le (S O) (S O)
             end of h2
             by (le_plus_plus . . . . h1 h2)
             we proved 
                le
                  plus (cweight c2) (S O)
                  plus (plus (cweight c2) (tweight t2)) (S O)
             by (lt_le_trans . . . H previous)
             we proved 
                lt
                  plus (cweight c1) (tweight t1)
                  plus (plus (cweight c2) (tweight t2)) (S O)
             that is equivalent to flt c1 t1 (CHead c2 __3 t2) (TLRef __1)
          we proved 
             lt (plus (cweight c1) (tweight t1)) (plus (cweight c2) (S O))
               →K→∀t2:T.nat→(flt c1 t1 (CHead c2 __3 t2) (TLRef __1))
          that is equivalent to (flt c1 t1 c2 (TLRef __1))→∀k2:K.∀t2:T.∀j:nat.(flt c1 t1 (CHead c2 k2 t2) (TLRef j))
       we proved 
          ∀c1:C
            .∀c2:C
              .∀t1:T
                .nat
                  →(flt c1 t1 c2 (TLRef __1))→∀k2:K.∀t2:T.∀j:nat.(flt c1 t1 (CHead c2 k2 t2) (TLRef j))