X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Funfold%2Fsstas_aaa.ma;h=b369caa723559093d5bc85d777db561d8331bf4c;hb=29973426e0227ee48368d1c24dc0c17bf2baef77;hp=36951ce083cc0c41f15897ffe5ba7b10533debe3;hpb=f95f6cb21b86f3dad114b21f687aa5df36088064;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/sstas_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/sstas_aaa.ma
index 36951ce08..b369caa72 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/unfold/sstas_aaa.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/sstas_aaa.ma
@@ -19,7 +19,7 @@ include "basic_2/unfold/sstas.ma".
 
 (* Properties on atomic arity assignment for terms **************************)
 
-lemma sstas_aaa: ∀h,g,L,T,U. ⦃h, L⦄ ⊢ T •*[g] U →
-                 ∀A. L ⊢ T ⁝ A → L ⊢ U ⁝ A.
+lemma sstas_aaa: ∀h,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/
 qed.