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 bB
        assume uT
        assume tT
        assume hnat
        assume dnat
          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)