X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fstatic%2Fssta_aaa.ma;h=eafec743074df4176a5556e70419f45a4e38b837;hb=8ff4315142253a1a0478b67c07dddf70c36f50cd;hp=01841483c7400ab33680a481b639d866c3eef7ab;hpb=7abd5e0412171f7d07e085d334198c034895c2c3;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/ssta_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/static/ssta_aaa.ma
index 01841483c..eafec7430 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/static/ssta_aaa.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/ssta_aaa.ma
@@ -19,7 +19,7 @@ include "basic_2/static/ssta.ma".
 
 (* Properties on atomic arity assignment for terms **************************)
 
-lemma ssta_aaa: ∀h,g,L,T,A. L ⊢ T ⁝ A → ∀U,l. ⦃h, L⦄ ⊢ T •[g, l] U → L ⊢ U ⁝ A.
+lemma ssta_aaa: ∀h,g,L,T,A. L ⊢ T ⁝ A → ∀U,l. ⦃h, L⦄ ⊢ T •[g] ⦃l, U⦄ → L ⊢ U ⁝ A.
 #h #g #L #T #A #H elim H -L -T -A
 [ #L #k #U #l #H
   elim (ssta_inv_sort1 … H) -H #_ #H destruct //