| lift_sort : ∀k,d,e. lift d e (⋆k) (⋆k)
| lift_lref_lt: ∀i,d,e. i < d → lift d e (#i) (#i)
| lift_lref_ge: ∀i,d,e. d ≤ i → lift d e (#i) (#(i + e))
| lift_sort : ∀k,d,e. lift d e (⋆k) (⋆k)
| lift_lref_lt: ∀i,d,e. i < d → lift d e (#i) (#i)
| lift_lref_ge: ∀i,d,e. d ≤ i → lift d e (#i) (#(i + e))