- lambdadelta: last recursive part of preservation finally proved!

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / static / ssta_aaa.ma

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 01841483c7400ab33680a481b639d866c3eef7ab..eafec743074df4176a5556e70419f45a4e38b837 100644 (file)
--- 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 //