lemma delift_fwd_lref1_be: ∀L,U2,d,e,i. L ⊢ #i [d, e] ≡ U2 →
d ≤ i → i < d + e →
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 &
#L #U2 #d #e #i * #U #HU #HU2 #Hdi #Hide
elim (tpss_inv_lref1 … HU) -HU
[ #H destruct elim (lift_inv_lref2_be … HU2 ? ?) //
#L #U2 #d #e #i * #U #HU #HU2 #Hdi #Hide
elim (tpss_inv_lref1 … HU) -HU
[ #H destruct elim (lift_inv_lref2_be … HU2 ? ?) //