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 =
Show proof