(* Basic properties *********************************************************)
-lemma delifta_lsubs_trans: ∀L1,T1,T2,d,e. L1 ⊢ ▼▼*[d, e] T1 ≡ T2 →
- â\88\80L2. L2 â\89¼ [d, e] L1 → L2 ⊢ ▼▼*[d, e] T1 ≡ T2.
+lemma delifta_lsubr_trans: ∀L1,T1,T2,d,e. L1 ⊢ ▼▼*[d, e] T1 ≡ T2 →
+ â\88\80L2. L2 â\8a\91 [d, e] L1 → L2 ⊢ ▼▼*[d, e] T1 ≡ 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_ldrop2_abbr … HL12 … HLK1 ? ?) -HL12 -HLK1 // /3 width=6/
+ elim (ldrop_lsubr_ldrop2_abbr … HL12 … HLK1 ? ?) -HL12 -HLK1 // /3 width=6/
| /4 width=1/
| /3 width=1/
]
]
| * [ #a ] #I #V1 #T1 #Hn #X #d #e #H
[ elim (delift_inv_bind1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct
- lapply (delift_lsubs_trans … HT12 (L.ⓑ{I}V1) ?) -HT12 /2 width=1/ #HT12
+ lapply (delift_lsubr_trans … HT12 (L.ⓑ{I}V1) ?) -HT12 /2 width=1/ #HT12
lapply (IH … HV12) -HV12 // #HV12
lapply (IH … HT12) -IH -HT12 /2 width=1/ #HT12
- lapply (delifta_lsubs_trans … HT12 (L.ⓑ{I}V2) ?) -HT12 /2 width=1/
+ lapply (delifta_lsubr_trans … HT12 (L.ⓑ{I}V2) ?) -HT12 /2 width=1/
| elim (delift_inv_flat1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct
lapply (IH … HV12) -HV12 //
lapply (IH … HT12) -IH -HT12 // /2 width=1/
lemma delifta_delift: ∀L,T1,T2,d,e. L ⊢ ▼▼*[d, e] T1 ≡ T2 → L ⊢ ▼*[d, e] T1 ≡ T2.
#L #T1 #T2 #d #e #H elim H -L -T1 -T2 -d -e // /2 width=1/ /2 width=6/
-qed-.
+qed-.
lemma delift_ind_alt: ∀R:ℕ→ℕ→lenv→relation term.
(∀L,d,e,k. R d e L (⋆k) (⋆k)) →
(∀L,d,e,i. i < d → R d e L (#i) (#i)) →
(∀L,K,V1,V2,W2,i,d,e. d ≤ i → i < d + e →
⇩[O, i] L ≡ K.ⓓV1 → K ⊢ ▼*[O, d + e - i - 1] V1 ≡ V2 →
- ⇧[O, d] V2 ≡ W2 → R O (d+e-i-1) K V1 V2 → R d e L #i W2
+ ⇧[O, d] V2 ≡ W2 → R O (d+e-i-1) K V1 V2 → R d e L (#i) W2
) →
(∀L,d,e,i. d + e ≤ i → R d e L (#i) (#(i - e))) →
(∀L,d,e,p. R d e L (§p) (§p)) →