-lemma csx_appl_simple_tsts: ∀h,g,G,L,V. ⦃G, L⦄ ⊢ ⬊*[h, g] V → ∀T1. ⦃G, L⦄ ⊢ ⬊*[h, g] T1 →
- (∀T2. ⦃G, L⦄ ⊢ T1 ➡*[h, g] T2 → (T1 ≂ T2 → ⊥) → ⦃G, L⦄ ⊢ ⬊*[h, g] ⓐV.T2) →
- 𝐒⦃T1⦄ → ⦃G, L⦄ ⊢ ⬊*[h, g] ⓐV.T1.
-#h #g #G #L #V #H @(csx_ind … H) -V #V #_ #IHV #T1 #H @(csx_ind … H) -T1 #T1 #H1T1 #IHT1 #H2T1 #H3T1
+lemma csx_appl_simple_tsts: ∀h,o,G,L,V. ⦃G, L⦄ ⊢ ⬊*[h, o] V → ∀T1. ⦃G, L⦄ ⊢ ⬊*[h, o] T1 →
+ (∀T2. ⦃G, L⦄ ⊢ T1 ➡*[h, o] T2 → (T1 ≂ T2 → ⊥) → ⦃G, L⦄ ⊢ ⬊*[h, o] ⓐV.T2) →
+ 𝐒⦃T1⦄ → ⦃G, L⦄ ⊢ ⬊*[h, o] ⓐV.T1.
+#h #o #G #L #V #H @(csx_ind … H) -V #V #_ #IHV #T1 #H @(csx_ind … H) -T1 #T1 #H1T1 #IHT1 #H2T1 #H3T1