DEFINITION subst0_tlt_head()
TYPE =
       ∀u:T
         .∀t:T
           .∀z:T
             .subst0 O u t z
               →tlt (THead (Bind Abbr) u z) (THead (Bind Abbr) u t)
BODY =
        assume u: T
        assume t: T
        assume z: T
        suppose H: subst0 O u t z
          (h1) 
             by (le_n .)
le (weight_map λ:nat.O u) (weight_map λ:nat.O u)
          end of h1
          (h2) 
             (h1) 
                assume m: nat
                   by (le_n .)
                   we proved 
                      le
                        wadd λ:nat.O (S (weight_map λ:nat.O u)) m
                        wadd λ:nat.O (S (weight_map λ:nat.O u)) m

                   ∀m:nat
                     .le
                       wadd λ:nat.O (S (weight_map λ:nat.O u)) m
                       wadd λ:nat.O (S (weight_map λ:nat.O u)) m
             end of h1
             (h2) 
                by (lift_weight_add_O . . . .)
                we proved 
                   eq
                     nat
                     weight_map λ:nat.O (lift O O u)
                     weight_map
                       wadd λ:nat.O (S (weight_map λ:nat.O u))
                       lift (S O) O u
                we proceed by induction on the previous result to prove 
                   lt
                     weight_map
                       wadd λ:nat.O (S (weight_map λ:nat.O u))
                       lift (S O) O u
                     S (weight_map λ:nat.O u)
                   case refl_equal : ⇒
                      the thesis becomes lt (weight_map λ:nat.O (lift O O u)) (S (weight_map λ:nat.O u))
                         (h1) 
                            by (le_n .)
                            we proved le (S (weight_map λ:nat.O u)) (S (weight_map λ:nat.O u))
lt (weight_map λ:nat.O u) (S (weight_map λ:nat.O u))
                         end of h1
                         (h2) 
                            by (lift_r . .)
eq T (lift O O u) u
                         end of h2
                         by (eq_ind_r . . . h1 . h2)
lt (weight_map λ:nat.O (lift O O u)) (S (weight_map λ:nat.O u))
                we proved 
                   lt
                     weight_map
                       wadd λ:nat.O (S (weight_map λ:nat.O u))
                       lift (S O) O u
                     S (weight_map λ:nat.O u)

                   lt
                     weight_map
                       wadd λ:nat.O (S (weight_map λ:nat.O u))
                       lift (S O) O u
                     wadd λ:nat.O (S (weight_map λ:nat.O u)) O
             end of h2
             by (subst0_weight_lt . . . . H . . h1 h2)

                lt
                  weight_map (wadd λ:nat.O (S (weight_map λ:nat.O u))) z
                  weight_map (wadd λ:nat.O (S (weight_map λ:nat.O u))) t
          end of h2
          by (le_lt_plus_plus . . . . h1 h2)
          we proved 
             lt
               plus
                 weight_map λ:nat.O u
                 weight_map (wadd λ:nat.O (S (weight_map λ:nat.O u))) z
               plus
                 weight_map λ:nat.O u
                 weight_map (wadd λ:nat.O (S (weight_map λ:nat.O u))) t
          by (lt_n_S . . previous)
          we proved 
             lt
               S
                 plus
                   weight_map λ:nat.O u
                   weight_map (wadd λ:nat.O (S (weight_map λ:nat.O u))) z
               S
                 plus
                   weight_map λ:nat.O u
                   weight_map (wadd λ:nat.O (S (weight_map λ:nat.O u))) t
          that is equivalent to tlt (THead (Bind Abbr) u z) (THead (Bind Abbr) u t)
       we proved 
          ∀u:T
            .∀t:T
              .∀z:T
                .subst0 O u t z
                  →tlt (THead (Bind Abbr) u z) (THead (Bind Abbr) u t)