qed.
(* Basic_2A1: uses: lsx_lref_skip *)
-lemma rsx_lref_unit_drops (h) (G): ∀I,L,K,i. ⇩*[i] L ≘ K.ⓤ[I] → G ⊢ ⬈*[h,#i] 𝐒❪L❫.
+lemma rsx_lref_unit_drops (h) (G): ∀I,L,K,i. ⇩[i] L ≘ K.ⓤ[I] → G ⊢ ⬈*[h,#i] 𝐒❪L❫.
#h #G #I #L1 #K1 #i #HL1
@(rsx_lifts … (#0) … HL1) -HL1 //
qed.
(* Basic_2A1: uses: lsx_fwd_lref_be *)
lemma rsx_fwd_lref_pair_drops (h) (G):
∀L,i. G ⊢ ⬈*[h,#i] 𝐒❪L❫ →
- ∀I,K,V. ⇩*[i] L ≘ K.ⓑ[I]V → G ⊢ ⬈*[h,V] 𝐒❪K❫.
+ ∀I,K,V. ⇩[i] L ≘ K.ⓑ[I]V → G ⊢ ⬈*[h,V] 𝐒❪K❫.
#h #G #L #i #HL #I #K #V #HLK
lapply (rsx_inv_lifts … HL … HLK … (#0) ?) -L
/2 width=2 by rsx_fwd_pair/