DEFINITION lift_r()
TYPE =
∀
t:
T
.
∀
d:
nat
.(
eq
T
(
lift
O
d t) t)
BODY =
Show proof