include "basic_2/unfold/delift_lift.ma".
-(* INVERSE TERM RELOCATION *************************************************)
+(* INVERSE BASIC TERM RELOCATION *******************************************)
-(* alternative definition of inverse relocation *)
+(* alternative definition of inverse basic term relocation *)
inductive delifta: nat → nat → lenv → relation term ≝
| delifta_sort : ∀L,d,e,k. delifta d e L (⋆k) (⋆k)
| delifta_lref_lt: ∀L,d,e,i. i < d → delifta d e L (#i) (#i)
delifta d e L (ⓕ{I} V1. T1) (ⓕ{I} V2. T2)
.
-interpretation "inverse relocation (term) alternative"
+interpretation "inverse basic relocation (term) alternative"
'TSubstAlt L T1 d e T2 = (delifta d e L T1 T2).
(* Basic properties *********************************************************)
lemma delifta_lsubs_conf: ∀L1,T1,T2,d,e. L1 ⊢ T1 [d, e] ≡≡ T2 →
- ∀L2. L1 [d, e] ≼ L2 → L2 ⊢ T1 [d, e] ≡≡ T2.
+ ∀L2. L1 ≼ [d, e] L2 → L2 ⊢ T1 [d, e] ≡≡ T2.
#L1 #T1 #T2 #d #e #H elim H -L1 -T1 -T2 -d -e // /2 width=1/
[ #L1 #K1 #V1 #V2 #W2 #i #d #e #Hdi #Hide #HLK1 #_ #HVW2 #IHV12 #L2 #HL12
elim (ldrop_lsubs_ldrop1_abbr … HL12 … HLK1 ? ?) -HL12 -HLK1 // /3 width=6/