DEFINITION flt_shift()
TYPE =
       ∀k:K.∀c:C.∀u:T.∀t:T.(flt (CHead c k u) t c (THead k u t))
BODY =
        assume : K
        assume c: C
        assume u: T
        assume t: T
          by (plus_n_Sm . .)
          we proved 
             eq
               nat
               S (plus (cweight c) (plus (tweight u) (tweight t)))
               plus (cweight c) (S (plus (tweight u) (tweight t)))
          we proceed by induction on the previous result to prove 
             lt
               plus (plus (cweight c) (tweight u)) (tweight t)
               plus (cweight c) (S (plus (tweight u) (tweight t)))
             case refl_equal : ⇒
                the thesis becomes 
                lt
                  plus (plus (cweight c) (tweight u)) (tweight t)
                  S (plus (cweight c) (plus (tweight u) (tweight t)))
                   (h1) 
                      by (le_n .)
                      we proved 
                         le
                           S (plus (plus (cweight c) (tweight u)) (tweight t))
                           S (plus (plus (cweight c) (tweight u)) (tweight t))

                         lt
                           plus (plus (cweight c) (tweight u)) (tweight t)
                           S (plus (plus (cweight c) (tweight u)) (tweight t))
                   end of h1
                   (h2) 
                      by (plus_assoc_l . . .)

                         eq
                           nat
                           plus (cweight c) (plus (tweight u) (tweight t))
                           plus (plus (cweight c) (tweight u)) (tweight t)
                   end of h2
                   by (eq_ind_r . . . h1 . h2)

                      lt
                        plus (plus (cweight c) (tweight u)) (tweight t)
                        S (plus (cweight c) (plus (tweight u) (tweight t)))
          we proved 
             lt
               plus (plus (cweight c) (tweight u)) (tweight t)
               plus (cweight c) (S (plus (tweight u) (tweight t)))
          that is equivalent to flt (CHead c __4 u) t c (THead __4 u t)
       we proved K→∀c:C.∀u:T.∀t:T.(flt (CHead c __4 u) t c (THead __4 u t))