- 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 d14083a45a1901f8b3ed2a1f500e03577ae4c346..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 //
@@ -38,4 +38,3 @@ lemma ssta_aaa: ∀h,g,L,T,A. L ⊢ T ⁝ A → ∀U,l. ⦃h, L⦄ ⊢ T •[g,
   lapply (ssta_inv_cast1 … H) -H /2 width=2/
 ]
 qed.
-