DEFINITION lift_gen_bind()
TYPE =
       ∀b:B
         .∀u:T
           .∀t:T
             .∀x:T
               .∀h:nat
                 .∀d:nat
                   .eq T (THead (Bind b) u t) (lift h d x)
                     →(ex3_2
                          T
                          T
                          λy:T.λz:T.eq T x (THead (Bind b) y z)
                          λy:T.λ:T.eq T u (lift h d y)
                          λ:T.λz:T.eq T t (lift h (S d) z))
BODY =
Show proof