-lemma csx_applv_theta: ∀h,o,p,G,L,V1b,V2b. ⬆*[1] V1b ≘ V2b →
- ∀V,T. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃ⓓ{p}V.ⒶV2b.T⦄ →
- ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃ⒶV1b.ⓓ{p}V.T⦄.
-#h #o #p #G #L #V1b #V2b * -V1b -V2b /2 width=1 by/
+lemma csx_applv_theta: ∀h,p,G,L,V1b,V2b. ⬆*[1] V1b ≘ V2b →
+ ∀V,T. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃ⓓ{p}V.ⒶV2b.T⦄ →
+ ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃ⒶV1b.ⓓ{p}V.T⦄.
+#h #p #G #L #V1b #V2b * -V1b -V2b /2 width=1 by/