-| 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_gref : ∀p,d,e. lift d e (§p) (§p)
-| lift_bind : ∀a,I,V1,V2,T1,T2,d,e.
- lift d e V1 V2 → lift (d + 1) e T1 T2 →
- lift d e (ⓑ{a,I} V1. T1) (ⓑ{a,I} V2. T2)
-| lift_flat : ∀I,V1,V2,T1,T2,d,e.
- lift d e V1 V2 → lift d e T1 T2 →
- lift d e (ⓕ{I} V1. T1) (ⓕ{I} V2. T2)
+| lift_sort : ∀k,l,m. lift l m (⋆k) (⋆k)
+| lift_lref_lt: ∀i,l,m. i < l → lift l m (#i) (#i)
+| lift_lref_ge: ∀i,l,m. l ≤ i → lift l m (#i) (#(i + m))
+| lift_gref : ∀p,l,m. lift l m (§p) (§p)
+| lift_bind : ∀a,I,V1,V2,T1,T2,l,m.
+ lift l m V1 V2 → lift (l + 1) m T1 T2 →
+ lift l m (ⓑ{a,I} V1. T1) (ⓑ{a,I} V2. T2)
+| lift_flat : ∀I,V1,V2,T1,T2,l,m.
+ lift l m V1 V2 → lift l m T1 T2 →
+ lift l m (ⓕ{I} V1. T1) (ⓕ{I} V2. T2)