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