DEFINITION flt_thead_dx()
TYPE =
       ∀k:K.∀c:C.∀u:T.∀t:T.(flt c t c (THead k u t))
BODY =
        assume : K
        assume c: C
        assume u: T
        assume t: T
          (h1) 
             by (le_n .)
le (cweight c) (cweight c)
          end of h1
          (h2) 
             by (le_plus_r . .)
             we proved le (tweight t) (plus (tweight u) (tweight t))
             by (le_n_S . . previous)
             we proved le (S (tweight t)) (S (plus (tweight u) (tweight t)))
lt (tweight t) (S (plus (tweight u) (tweight t)))
          end of h2
          by (le_lt_plus_plus . . . . h1 h2)
          we proved 
             lt
               plus (cweight c) (tweight t)
               plus (cweight c) (S (plus (tweight u) (tweight t)))
          that is equivalent to flt c t c (THead __4 u t)
       we proved K→∀c:C.∀u:T.∀t:T.(flt c t c (THead __4 u t))