fact sfr_delift_aux: ∀L,T,T1,d,e. d + e ≤ |L| → ≽ [d, e] L → T = T1 →
∃T2. L ⊢ ▼*[d, e] T1 ≡ T2.
fact sfr_delift_aux: ∀L,T,T1,d,e. d + e ≤ |L| → ≽ [d, e] L → T = T1 →
∃T2. L ⊢ ▼*[d, e] T1 ≡ T2.
[ #i #d #e #Hde #HL #H destruct
elim (lt_or_ge i d) #Hdi [ /3 width=2/ ]
elim (lt_or_ge i (d+e)) #Hide [2: /3 width=2/ ]
lapply (lt_to_le_to_lt … Hide Hde) #Hi
elim (ldrop_O1_lt … Hi) -Hi #I #K #V1 #HLK
lapply (sfr_inv_ldrop … HLK … HL ? ?) // #H destruct
[ #i #d #e #Hde #HL #H destruct
elim (lt_or_ge i d) #Hdi [ /3 width=2/ ]
elim (lt_or_ge i (d+e)) #Hide [2: /3 width=2/ ]
lapply (lt_to_le_to_lt … Hide Hde) #Hi
elim (ldrop_O1_lt … Hi) -Hi #I #K #V1 #HLK
lapply (sfr_inv_ldrop … HLK … HL ? ?) // #H destruct
lapply (ldrop_fwd_ldrop2 … HLK) #HLK0
lapply (ldrop_fwd_O1_length … HLK0) #H
lapply (sfr_ldrop_trans_be_up … HLK0 … HL ? ?) -HLK0 -HL
lapply (ldrop_fwd_ldrop2 … HLK) #HLK0
lapply (ldrop_fwd_O1_length … HLK0) #H
lapply (sfr_ldrop_trans_be_up … HLK0 … HL ? ?) -HLK0 -HL