-lemma snv_sstas_fwd_correct: ∀h,g,L,T1,T2. ⦃h, L⦄ ⊢ T1 ¡[g] → ⦃h, L⦄ ⊢ T1 •* [g] T2 →
- ∃∃U2,l. ⦃h, L⦄ ⊢ T2 •[g] ⦃l, U2⦄.
+lemma snv_sstas_fwd_correct: ∀h,g,L,T1,T2. ⦃G, L⦄ ⊢ T1 ¡[h, g] → ⦃G, L⦄ ⊢ T1 •* [h, g] T2 →
+ ∃∃U2,l. ⦃G, L⦄ ⊢ T2 •[h, g] ⦃l, U2⦄.