DEFINITION lift()
TYPE =
       nat→nat→T→T
BODY =
λh:nat.λi:nat.λt:T.lref_map λx:nat.plus x h i t