-fact rdsx_bind_lpxs_void_aux (h) (o) (G):
- ∀p,I,L1,V. G ⊢ ⬈*[h, o, V] 𝐒⦃L1⦄ →
- ∀Y,T. G ⊢ ⬈*[h, o, T] 𝐒⦃Y⦄ →
- ∀L2. Y = L2.ⓧ → ⦃G, L1⦄ ⊢ ⬈*[h] L2 →
- G ⊢ ⬈*[h, o, ⓑ{p,I}V.T] 𝐒⦃L2⦄.
-#h #o #G #p #I #L1 #V #H @(rdsx_ind_lpxs … H) -L1
+fact rdsx_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 @(rdsx_ind_lpxs … H) -L1