(* GENERIC TERM RELOCATION **************************************************)
inductive lifts: list2 nat nat → relation term ≝
-| lifts_nil : â\88\80T. lifts (â\9f ) T T
+| lifts_nil : â\88\80T. lifts (â\97\8a) T T
| lifts_cons: ∀T1,T,T2,des,d,e.
⇧[d,e] T1 ≡ T → lifts des T T2 → lifts ({d, e} @ des) T1 T2
.
(* Basic inversion lemmas ***************************************************)
-fact lifts_inv_nil_aux: â\88\80T1,T2,des. â\87§*[des] T1 â\89¡ T2 â\86\92 des = â\9f → T1 = T2.
+fact lifts_inv_nil_aux: â\88\80T1,T2,des. â\87§*[des] T1 â\89¡ T2 â\86\92 des = â\97\8a → T1 = T2.
#T1 #T2 #des * -T1 -T2 -des //
#T1 #T #T2 #d #e #des #_ #_ #H destruct
qed-.
-lemma lifts_inv_nil: â\88\80T1,T2. â\87§*[â\9f ] T1 ≡ T2 → T1 = T2.
+lemma lifts_inv_nil: â\88\80T1,T2. â\87§*[â\97\8a] T1 ≡ T2 → T1 = T2.
/2 width=3 by lifts_inv_nil_aux/ qed-.
fact lifts_inv_cons_aux: ∀T1,T2,des. ⇧*[des] T1 ≡ T2 →