DEFINITION lift_bind()
TYPE =
       ∀b:B
         .∀u:T
           .∀t:T
             .∀h:nat
               .∀d:nat
                 .eq
                   T
                   lift h d (THead (Bind b) u t)
                   THead (Bind b) (lift h d u) (lift h (S d) t)
BODY =
        assume b: B
        assume u: T
        assume t: T
        assume h: nat
        assume d: nat
          by (refl_equal . .)
          we proved 
             eq
               T
               THead (Bind b) (lift h d u) (lift h (S d) t)
               THead (Bind b) (lift h d u) (lift h (S d) t)
          that is equivalent to 
             eq
               T
               lift h d (THead (Bind b) u t)
               THead (Bind b) (lift h d u) (lift h (S d) t)
       we proved 
          ∀b:B
            .∀u:T
              .∀t:T
                .∀h:nat
                  .∀d:nat
                    .eq
                      T
                      lift h d (THead (Bind b) u t)
                      THead (Bind b) (lift h d u) (lift h (S d) t)