-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.