-lemma ssta_aaa: ∀h,g,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → ∀U,l. ⦃G, L⦄ ⊢ T •[h, g] ⦃l, U⦄ → ⦃G, L⦄ ⊢ U ⁝ A.
-#h #g #L #T #A #H elim H -L -T -A
-[ #L #k #U #l #H
+lemma ssta_aaa: ∀h,g,G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → ∀U,l. ⦃G, L⦄ ⊢ T •[h, g] ⦃l, U⦄ → ⦃G, L⦄ ⊢ U ⁝ A.
+#h #g #G #L #T #A #H elim H -G -L -T -A
+[ #G #L #k #U #l #H