-lemma csx_appl_simple_theq: ∀h,G,L,V. ⦃G, L⦄ ⊢ ⬈*[h] 𝐒⦃V⦄ → ∀T1. ⦃G, L⦄ ⊢ ⬈*[h] 𝐒⦃T1⦄ →
- (∀T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 → (T1 ⩳ T2 → ⊥) → ⦃G, L⦄ ⊢ ⬈*[h] 𝐒⦃ⓐV.T2⦄) →
- 𝐒⦃T1⦄ → ⦃G, L⦄ ⊢ ⬈*[h] 𝐒⦃ⓐV.T1⦄.
+lemma csx_appl_simple_theq: ∀h,G,L,V. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃V⦄ → ∀T1. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃T1⦄ →
+ (∀T2. ⦃G,L⦄ ⊢ T1 ⬈*[h] T2 → (T1 ⩳ T2 → ⊥) → ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃ⓐV.T2⦄) →
+ 𝐒⦃T1⦄ → ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃ⓐV.T1⦄.