DEFINITION flt_thead_sx()
TYPE =
       ∀k:K.∀c:C.∀u:T.∀t:T.(flt c u 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_l . .)
             we proved le (tweight u) (plus (tweight u) (tweight t))
             by (le_n_S . . previous)
             we proved le (S (tweight u)) (S (plus (tweight u) (tweight t)))
lt (tweight u) (S (plus (tweight u) (tweight t)))
          end of h2
          by (le_lt_plus_plus . . . . h1 h2)
          we proved 
             lt
               plus (cweight c) (tweight u)
               plus (cweight c) (S (plus (tweight u) (tweight t)))
          that is equivalent to flt c u c (THead __4 u t)
       we proved K→∀c:C.∀u:T.∀t:T.(flt c u c (THead __4 u t))