lemma delift_fwd_lref1_be: ∀L,U2,d,e,i. L ⊢ #i [d, e] ≡ U2 →
d ≤ i → i < d + e →
- â\88\83â\88\83K,V1,V2. â\87\93[0, i] L â\89¡ K. ð\9d\95\93{Abbr} V1 &
+ â\88\83â\88\83K,V1,V2. â\87©[0, i] L â\89¡ K. â\93\93V1 &
K ⊢ V1 [0, d + e - i - 1] ≡ V2 &
- â\87\91[0, d] V2 ≡ U2.
+ â\87§[0, d] V2 ≡ U2.
#L #U2 #d #e #i * #U #HU #HU2 #Hdi #Hide
elim (tpss_inv_lref1 … HU) -HU
[ #H destruct elim (lift_inv_lref2_be … HU2 ? ?) //