DEFINITION lift_gen_head()
TYPE =
       ∀k:K
         .∀u:T
           .∀t:T
             .∀x:T
               .∀h:nat
                 .∀d:nat
                   .eq T (THead k u t) (lift h d x)
                     →(ex3_2
                          T
                          T
                          λy:T.λz:T.eq T x (THead k y z)
                          λy:T.λ:T.eq T u (lift h d y)
                          λ:T.λz:T.eq T t (lift h (s k d) z))
BODY =
Show proof