DEFINITION tlt_head_sx()
TYPE =
       ∀k:K.∀u:T.∀t:T.(tlt u (THead k u t))
BODY =
       assume k: K
          we proceed by induction on k to prove 
             ∀u:T.∀t:T.(lt (weight_map λ:nat.O u) (weight_map λ:nat.O (THead k u t)))
             case Bind : b:B ⇒
                the thesis becomes 
                ∀u:T
                  .∀t:T
                    .lt
                      weight_map λ:nat.O u
                      weight_map λ:nat.O (THead (Bind b) u t)
                   we proceed by induction on b to prove 
                      ∀u:T
                        .∀t:T
                          .lt
                            weight_map λ:nat.O u
                            <λb1:B.nat>
                              CASE b OF
                                Abbr⇒
                                    S
                                      plus
                                        weight_map λ:nat.O u
                                        weight_map (wadd λ:nat.O (S (weight_map λ:nat.O u))) t
                              | Abst⇒S (plus (weight_map λ:nat.O u) (weight_map (wadd λ:nat.O O) t))
                              | Void⇒S (plus (weight_map λ:nat.O u) (weight_map (wadd λ:nat.O O) t))
                      case Abbr : ⇒
                         the thesis becomes 
                         ∀u:T
                           .∀t:T
                             .lt
                               weight_map λ:nat.O u
                               <λb1:B.nat>
                                 CASE Abbr OF
                                   Abbr⇒
                                       S
                                         plus
                                           weight_map λ:nat.O u
                                           weight_map (wadd λ:nat.O (S (weight_map λ:nat.O u))) t
                                 | Abst⇒S (plus (weight_map λ:nat.O u) (weight_map (wadd λ:nat.O O) t))
                                 | Void⇒S (plus (weight_map λ:nat.O u) (weight_map (wadd λ:nat.O O) t))
                             assume u: T
                             assume t: T
                               by (le_plus_l . .)
                               we proved 
                                  le
                                    weight_map λ:nat.O u
                                    plus
                                      weight_map λ:nat.O u
                                      weight_map (wadd λ:nat.O (S (weight_map λ:nat.O u))) t
                               by (le_n_S . . previous)
                               we proved 
                                  le
                                    S (weight_map λ:nat.O u)
                                    S
                                      plus
                                        weight_map λ:nat.O u
                                        weight_map (wadd λ:nat.O (S (weight_map λ:nat.O u))) t
                               that is equivalent to 
                                  lt
                                    weight_map λ:nat.O u
                                    <λb1:B.nat>
                                      CASE Abbr OF
                                        Abbr⇒
                                            S
                                              plus
                                                weight_map λ:nat.O u
                                                weight_map (wadd λ:nat.O (S (weight_map λ:nat.O u))) t
                                      | Abst⇒S (plus (weight_map λ:nat.O u) (weight_map (wadd λ:nat.O O) t))
                                      | Void⇒S (plus (weight_map λ:nat.O u) (weight_map (wadd λ:nat.O O) t))

                               ∀u:T
                                 .∀t:T
                                   .lt
                                     weight_map λ:nat.O u
                                     <λb1:B.nat>
                                       CASE Abbr OF
                                         Abbr⇒
                                             S
                                               plus
                                                 weight_map λ:nat.O u
                                                 weight_map (wadd λ:nat.O (S (weight_map λ:nat.O u))) t
                                       | Abst⇒S (plus (weight_map λ:nat.O u) (weight_map (wadd λ:nat.O O) t))
                                       | Void⇒S (plus (weight_map λ:nat.O u) (weight_map (wadd λ:nat.O O) t))
                      case Abst : ⇒
                         the thesis becomes 
                         ∀u:T
                           .∀t:T
                             .lt
                               weight_map λ:nat.O u
                               <λb1:B.nat>
                                 CASE Abst OF
                                   Abbr⇒
                                       S
                                         plus
                                           weight_map λ:nat.O u
                                           weight_map (wadd λ:nat.O (S (weight_map λ:nat.O u))) t
                                 | Abst⇒S (plus (weight_map λ:nat.O u) (weight_map (wadd λ:nat.O O) t))
                                 | Void⇒S (plus (weight_map λ:nat.O u) (weight_map (wadd λ:nat.O O) t))
                             assume u: T
                             assume t: T
                               by (le_plus_l . .)
                               we proved 
                                  le
                                    weight_map λ:nat.O u
                                    plus (weight_map λ:nat.O u) (weight_map (wadd λ:nat.O O) t)
                               by (le_n_S . . previous)
                               we proved 
                                  le
                                    S (weight_map λ:nat.O u)
                                    S (plus (weight_map λ:nat.O u) (weight_map (wadd λ:nat.O O) t))
                               that is equivalent to 
                                  lt
                                    weight_map λ:nat.O u
                                    <λb1:B.nat>
                                      CASE Abst OF
                                        Abbr⇒
                                            S
                                              plus
                                                weight_map λ:nat.O u
                                                weight_map (wadd λ:nat.O (S (weight_map λ:nat.O u))) t
                                      | Abst⇒S (plus (weight_map λ:nat.O u) (weight_map (wadd λ:nat.O O) t))
                                      | Void⇒S (plus (weight_map λ:nat.O u) (weight_map (wadd λ:nat.O O) t))

                               ∀u:T
                                 .∀t:T
                                   .lt
                                     weight_map λ:nat.O u
                                     <λb1:B.nat>
                                       CASE Abst OF
                                         Abbr⇒
                                             S
                                               plus
                                                 weight_map λ:nat.O u
                                                 weight_map (wadd λ:nat.O (S (weight_map λ:nat.O u))) t
                                       | Abst⇒S (plus (weight_map λ:nat.O u) (weight_map (wadd λ:nat.O O) t))
                                       | Void⇒S (plus (weight_map λ:nat.O u) (weight_map (wadd λ:nat.O O) t))
                      case Void : ⇒
                         the thesis becomes 
                         ∀u:T
                           .∀t:T
                             .lt
                               weight_map λ:nat.O u
                               <λb1:B.nat>
                                 CASE Void OF
                                   Abbr⇒
                                       S
                                         plus
                                           weight_map λ:nat.O u
                                           weight_map (wadd λ:nat.O (S (weight_map λ:nat.O u))) t
                                 | Abst⇒S (plus (weight_map λ:nat.O u) (weight_map (wadd λ:nat.O O) t))
                                 | Void⇒S (plus (weight_map λ:nat.O u) (weight_map (wadd λ:nat.O O) t))
                             assume u: T
                             assume t: T
                               by (le_plus_l . .)
                               we proved 
                                  le
                                    weight_map λ:nat.O u
                                    plus (weight_map λ:nat.O u) (weight_map (wadd λ:nat.O O) t)
                               by (le_n_S . . previous)
                               we proved 
                                  le
                                    S (weight_map λ:nat.O u)
                                    S (plus (weight_map λ:nat.O u) (weight_map (wadd λ:nat.O O) t))
                               that is equivalent to 
                                  lt
                                    weight_map λ:nat.O u
                                    <λb1:B.nat>
                                      CASE Void OF
                                        Abbr⇒
                                            S
                                              plus
                                                weight_map λ:nat.O u
                                                weight_map (wadd λ:nat.O (S (weight_map λ:nat.O u))) t
                                      | Abst⇒S (plus (weight_map λ:nat.O u) (weight_map (wadd λ:nat.O O) t))
                                      | Void⇒S (plus (weight_map λ:nat.O u) (weight_map (wadd λ:nat.O O) t))

                               ∀u:T
                                 .∀t:T
                                   .lt
                                     weight_map λ:nat.O u
                                     <λb1:B.nat>
                                       CASE Void OF
                                         Abbr⇒
                                             S
                                               plus
                                                 weight_map λ:nat.O u
                                                 weight_map (wadd λ:nat.O (S (weight_map λ:nat.O u))) t
                                       | Abst⇒S (plus (weight_map λ:nat.O u) (weight_map (wadd λ:nat.O O) t))
                                       | Void⇒S (plus (weight_map λ:nat.O u) (weight_map (wadd λ:nat.O O) t))
                   we proved 
                      ∀u:T
                        .∀t:T
                          .lt
                            weight_map λ:nat.O u
                            <λb1:B.nat>
                              CASE b OF
                                Abbr⇒
                                    S
                                      plus
                                        weight_map λ:nat.O u
                                        weight_map (wadd λ:nat.O (S (weight_map λ:nat.O u))) t
                              | Abst⇒S (plus (weight_map λ:nat.O u) (weight_map (wadd λ:nat.O O) t))
                              | Void⇒S (plus (weight_map λ:nat.O u) (weight_map (wadd λ:nat.O O) t))

                      ∀u:T
                        .∀t:T
                          .lt
                            weight_map λ:nat.O u
                            weight_map λ:nat.O (THead (Bind b) u t)
             case Flat : :F ⇒
                the thesis becomes 
                ∀u:T
                  .∀t:T
                    .le
                      S (weight_map λ:nat.O u)
                      S (plus (weight_map λ:nat.O u) (weight_map λ:nat.O t))
                    assume u: T
                    assume t: T
                      by (le_plus_l . .)
                      we proved 
                         le
                           weight_map λ:nat.O u
                           plus (weight_map λ:nat.O u) (weight_map λ:nat.O t)
                      by (le_n_S . . previous)
                      we proved 
                         le
                           S (weight_map λ:nat.O u)
                           S (plus (weight_map λ:nat.O u) (weight_map λ:nat.O t))
                      that is equivalent to 
                         lt
                           weight_map λ:nat.O u
                           weight_map λ:nat.O (THead (Flat __3) u t)

                      ∀u:T
                        .∀t:T
                          .le
                            S (weight_map λ:nat.O u)
                            S (plus (weight_map λ:nat.O u) (weight_map λ:nat.O t))
          we proved 
             ∀u:T.∀t:T.(lt (weight_map λ:nat.O u) (weight_map λ:nat.O (THead k u t)))
          that is equivalent to ∀u:T.∀t:T.(tlt u (THead k u t))
       we proved ∀k:K.∀u:T.∀t:T.(tlt u (THead k u t))