(* *)
(**************************************************************************)
-include "Basic_2/substitution/lift.ma".
-include "Basic_2/unfold/gr2_plus.ma".
+include "basic_2/substitution/lift.ma".
+include "basic_2/unfold/gr2_plus.ma".
(* GENERIC TERM RELOCATION **************************************************)
inductive lifts: list2 nat nat → relation term ≝
| lifts_nil : ∀T. lifts ⟠ T T
| lifts_cons: ∀T1,T,T2,des,d,e.
- ⇧[d,e] T1 ≡ T → lifts des T T2 → lifts ({d, e} :: des) T1 T2
+ ⇧[d,e] T1 ≡ T → lifts des T T2 → lifts ({d, e} @ des) T1 T2
.
interpretation "generic relocation (term)"
/2 width=3/ qed-.
fact lifts_inv_cons_aux: ∀T1,T2,des. ⇧*[des] T1 ≡ T2 →
- ∀d,e,tl. des = {d, e} :: tl →
+ ∀d,e,tl. des = {d, e} @ tl →
∃∃T. ⇧[d, e] T1 ≡ T & ⇧*[tl] T ≡ T2.
#T1 #T2 #des * -T1 -T2 -des
[ #T #d #e #tl #H destruct
/2 width=3/
qed.
-lemma lifts_inv_cons: ∀T1,T2,d,e,des. ⇧*[{d, e} :: des] T1 ≡ T2 →
+lemma lifts_inv_cons: ∀T1,T2,d,e,des. ⇧*[{d, e} @ des] T1 ≡ T2 →
∃∃T. ⇧[d, e] T1 ≡ T & ⇧*[des] T ≡ T2.
/2 width=3/ qed-.
(* Basic forward lemmas *****************************************************)
-lemma lifts_simple_dx: ∀T1,T2,des. ⇧*[des] T1 ≡ T2 → 𝐒[T1] → 𝐒[T2].
+lemma lifts_simple_dx: ∀T1,T2,des. ⇧*[des] T1 ≡ T2 → 𝐒⦃T1⦄ → 𝐒⦃T2⦄.
#T1 #T2 #des #H elim H -T1 -T2 -des // /3 width=5 by lift_simple_dx/
qed-.
-lemma lifts_simple_sn: ∀T1,T2,des. ⇧*[des] T1 ≡ T2 → 𝐒[T2] → 𝐒[T1].
+lemma lifts_simple_sn: ∀T1,T2,des. ⇧*[des] T1 ≡ T2 → 𝐒⦃T2⦄ → 𝐒⦃T1⦄.
#T1 #T2 #des #H elim H -T1 -T2 -des // /3 width=5 by lift_simple_sn/
qed-.