| lifts_lref: ∀f,i1,i2. @⦃i1, f⦄ ≘ i2 → lifts f (#i1) (#i2)
| lifts_gref: ∀f,l. lifts f (§l) (§l)
| lifts_bind: ∀f,p,I,V1,V2,T1,T2.
| lifts_lref: ∀f,i1,i2. @⦃i1, f⦄ ≘ i2 → lifts f (#i1) (#i2)
| lifts_gref: ∀f,l. lifts f (§l) (§l)
| lifts_bind: ∀f,p,I,V1,V2,T1,T2.