-lemma csn_appl_simple: ∀h,g,L,V. ⦃h, L⦄ ⊢ ⬊*[g] V → ∀T1.
- (∀T2. ⦃h, L⦄ ⊢ T1 ➡[g] T2 → (T1 = T2 → ⊥) → ⦃h, L⦄ ⊢ ⬊*[g] ⓐV.T2) →
- 𝐒⦃T1⦄ → ⦃h, L⦄ ⊢ ⬊*[g] ⓐV.T1.
+lemma csn_appl_simple: ∀h,g,L,V. ⦃G, L⦄ ⊢ ⬊*[h, g] V → ∀T1.
+ (∀T2. ⦃G, L⦄ ⊢ T1 ➡[h, g] T2 → (T1 = T2 → ⊥) → ⦃G, L⦄ ⊢ ⬊*[h, g] ⓐV.T2) →
+ 𝐒⦃T1⦄ → ⦃G, L⦄ ⊢ ⬊*[h, g] ⓐV.T1.