-fact rsx_bind_lpxs_void_aux (h) (G):
- ∀p,I,L1,V. G ⊢ ⬈*[h,V] 𝐒❪L1❫ →
- ∀Y,T. G ⊢ ⬈*[h,T] 𝐒❪Y❫ →
- ∀L2. Y = L2.ⓧ → ❪G,L1❫ ⊢ ⬈*[h] L2 →
- G ⊢ ⬈*[h,ⓑ[p,I]V.T] 𝐒❪L2❫.
-#h #G #p #I #L1 #V #H @(rsx_ind_lpxs … H) -L1
+fact rsx_bind_lpxs_void_aux (G):
+ ∀p,I,L1,V. G ⊢ ⬈*𝐒[V] L1 →
+ ∀Y,T. G ⊢ ⬈*𝐒[T] Y →
+ ∀L2. Y = L2.ⓧ → ❪G,L1❫ ⊢ ⬈* L2 →
+ G ⊢ ⬈*𝐒[ⓑ[p,I]V.T] L2.
+#G #p #I #L1 #V #H @(rsx_ind_lpxs … H) -L1