| lifts_sort: ∀f,s. lifts f (⋆s) (⋆s)
| lifts_lref: ∀f,i1,i2. @❪i1,f❫ ≘ i2 → lifts f (#i1) (#i2)
| lifts_gref: ∀f,l. lifts f (§l) (§l)
| lifts_sort: ∀f,s. lifts f (⋆s) (⋆s)
| lifts_lref: ∀f,i1,i2. @❪i1,f❫ ≘ i2 → lifts f (#i1) (#i2)
| lifts_gref: ∀f,l. lifts f (§l) (§l)