(* GENERIC TERM RELOCATION **************************************************)
inductive lifts: mr2 → relation term ≝
-| lifts_nil : ∀T. lifts (◊) T T
+| lifts_nil : ∀T. lifts (𝐞) T T
| lifts_cons: ∀T1,T,T2,cs,l,m.
⬆[l,m] T1 ≡ T → lifts cs T T2 → lifts (❨l, m❩; cs) T1 T2
.
(* Basic inversion lemmas ***************************************************)
-fact lifts_inv_nil_aux: ∀T1,T2,cs. ⬆*[cs] T1 ≡ T2 → cs = ◊ → T1 = T2.
+fact lifts_inv_nil_aux: ∀T1,T2,cs. ⬆*[cs] T1 ≡ T2 → cs = 𝐞 → T1 = T2.
#T1 #T2 #cs * -T1 -T2 -cs //
#T1 #T #T2 #l #m #cs #_ #_ #H destruct
qed-.
-lemma lifts_inv_nil: ∀T1,T2. ⬆*[◊] T1 ≡ T2 → T1 = T2.
+lemma lifts_inv_nil: ∀T1,T2. ⬆*[𝐞] T1 ≡ T2 → T1 = T2.
/2 width=3 by lifts_inv_nil_aux/ qed-.
fact lifts_inv_cons_aux: ∀T1,T2,cs. ⬆*[cs] T1 ≡ T2 →