-lemma rdsx_flat_lpxs (h) (o) (G):
- ∀I,L1,V. G ⊢ ⬈*[h, o, V] 𝐒⦃L1⦄ →
- ∀L2,T. G ⊢ ⬈*[h, o, T] 𝐒⦃L2⦄ → ⦃G, L1⦄ ⊢ ⬈*[h] L2 →
- G ⊢ ⬈*[h, o, ⓕ{I}V.T] 𝐒⦃L2⦄.
-#h #o #G #I #L1 #V #H @(rdsx_ind_lpxs … H) -L1
+lemma rdsx_flat_lpxs (h) (G):
+ ∀I,L1,V. G ⊢ ⬈*[h, V] 𝐒⦃L1⦄ →
+ ∀L2,T. G ⊢ ⬈*[h, T] 𝐒⦃L2⦄ → ⦃G, L1⦄ ⊢ ⬈*[h] L2 →
+ G ⊢ ⬈*[h, ⓕ{I}V.T] 𝐒⦃L2⦄.
+#h #G #I #L1 #V #H @(rdsx_ind_lpxs … H) -L1