DEFINITION pr0_gen_lift()
TYPE =
       ∀t1:T.∀x:T.∀h:nat.∀d:nat.(pr0 (lift h d t1) x)→(ex2 T λt2:T.eq T x (lift h d t2) λt2:T.pr0 t1 t2)
BODY =
Show proof