DEFINITION pc3_gen_lift_abst()
TYPE =
       ∀c:C
         .∀t:T
           .∀t2:T
             .∀u2:T
               .∀h:nat
                 .∀d:nat
                   .pc3 c (lift h d t) (THead (Bind Abst) u2 t2)
                     →∀e:C
                          .drop h d c e
                            →(ex3_2
                                 T
                                 T
                                 λu1:T.λt1:T.pr3 e t (THead (Bind Abst) u1 t1)
                                 λu1:T.λ:T.pr3 c u2 (lift h d u1)
                                 λ:T.λt1:T.∀b:B.∀u:T.(pr3 (CHead c (Bind b) u) t2 (lift h (S d) t1)))
BODY =
Show proof