DEFINITION pr0_lift()
TYPE =
       ∀t1:T.∀t2:T.(pr0 t1 t2)→∀h:nat.∀d:nat.(pr0 (lift h d t1) (lift h d t2))
BODY =
Show proof