DEFINITION flt_arith0()
TYPE =
       ∀k:K.∀c:C.∀t:T.∀i:nat.(flt c t (CHead c k t) (TLRef i))
BODY =
        assume : K
        assume c: C
        assume t: T
        assume : nat
          by (lt_x_plus_x_Sy . .)
          we proved 
             lt
               plus (cweight c) (tweight t)
               plus (plus (cweight c) (tweight t)) (S O)
          that is equivalent to flt c t (CHead c __4 t) (TLRef __1)
       we proved K→∀c:C.∀t:T.nat→(flt c t (CHead c __4 t) (TLRef __1))