λf. ext2 (lifts f).
interpretation "generic relocation (binder for local environments)"
'RLiftStar f I1 I2 = (liftsb f I1 I2).
interpretation "uniform relocation (binder for local environments)"
λf. ext2 (lifts f).
interpretation "generic relocation (binder for local environments)"
'RLiftStar f I1 I2 = (liftsb f I1 I2).
interpretation "uniform relocation (binder for local environments)"