(* Properties on atomic arity assignment for terms **************************)
-lemma sstas_aaa: ∀h,g,L,T,U. ⦃G, L⦄ ⊢ T •*[h, g] U →
+lemma sstas_aaa: ∀h,g,G,L,T,U. ⦃G, L⦄ ⊢ T •*[h, g] U →
∀A. ⦃G, L⦄ ⊢ T ⁝ A → ⦃G, L⦄ ⊢ U ⁝ A.
-#h #g #L #T #U #H @(sstas_ind_dx … H) -T // /3 width=6/
+#h #g #G #L #T #U #H @(sstas_ind_dx … H) -T // /3 width=6/
qed.