+lemma cpys_inv_lref1_ldrop: ∀G,L,T2,i,d,e. ⦃G, L⦄ ⊢ #i ▶*[d, e] T2 →
+ ∀I,K,V1. ⇩[i] L ≡ K.ⓑ{I}V1 →
+ ∀V2. ⇧[O, i+1] V2 ≡ T2 →
+ ∧∧ ⦃G, K⦄ ⊢ V1 ▶*[0, ⫰(d+e-i)] V2
+ & d ≤ i
+ & i < d + e.
+#G #L #T2 #i #d #e #H #I #K #V1 #HLK #V2 #HVT2 elim (cpys_inv_lref1 … H) -H
+[ #H destruct elim (lift_inv_lref2_be … HVT2) -HVT2 -HLK //
+| * #Z #Y #X1 #X2 #Hdi #Hide #HLY #HX12 #HXT2
+ lapply (lift_inj … HXT2 … HVT2) -T2 #H destruct
+ lapply (ldrop_mono … HLY … HLK) -L #H destruct
+ /2 width=1 by and3_intro/
+]
+qed-.
+
+(* Properties on relocation *************************************************)