-fact rsx_bind_lpxs_void_aux (h) (G):
- ∀p,I,L1,V. G ⊢ ⬈*[h,V] 𝐒⦃L1⦄ →
- ∀Y,T. G ⊢ ⬈*[h,T] 𝐒⦃Y⦄ →
- â\88\80L2. Y = L2.â\93§ â\86\92 â¦\83G,L1â¦\84 â\8a¢ â¬\88*[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 →
+ â\88\80L2. Y = L2.â\93§ â\86\92 â\9dªG,L1â\9d« â\8a¢ â¬\88* L2 →
+ G ⊢ ⬈*𝐒[ⓑ[p,I]V.T] L2.
+#G #p #I #L1 #V #H @(rsx_ind_lpxs … H) -L1