(* GENERIC RELOCATION FOR BINDERS *******************************************)
-definition liftsb: rtmap → relation bind ≝
+definition liftsb: pr_map → relation bind ≝
λ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)"
- 'RLift i I1 I2 = (liftsb (uni i) I1 I2).
+ 'RLift i I1 I2 = (liftsb (pr_uni i) I1 I2).
(* Basic_inversion lemmas **************************************************)
(* Basic properties *********************************************************)
-lemma liftsb_eq_repl_back: ∀I1,I2. eq_repl_back … (λf. ⇧*[f] I1 ≘ I2).
+lemma liftsb_eq_repl_back: ∀I1,I2. pr_eq_repl_back … (λf. ⇧*[f] I1 ≘ I2).
#I1 #I2 #f1 * -I1 -I2 /3 width=3 by lifts_eq_repl_back, ext2_pair/
qed-.