X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fcomputation%2Fcsn_aaa.ma;h=cd8d5a64b7ef7df7aeb11c29221b6734db04597f;hb=f95f6cb21b86f3dad114b21f687aa5df36088064;hp=109d9301849230598b34de25da15422dac0828c7;hpb=08cb57944c0df08611d4f35d286e46c0d13e4813;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csn_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csn_aaa.ma
index 109d93018..cd8d5a64b 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/csn_aaa.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/csn_aaa.ma
@@ -15,11 +15,11 @@
 include "basic_2/computation/acp_aaa.ma".
 include "basic_2/computation/csn_tstc_vector.ma".
 
-(* CONTEXT-SENSITIVE STRONGLY NORMALIZING TERMS *****************************)
+(* CONTEXT-SENSITIVE EXTENDED STRONGLY NORMALIZING TERMS ********************)
 
-(* Properties concerning atomic arity assignment ****************************)
+(* Main properties concerning atomic arity assignment ***********************)
 
-lemma csn_aaa: ∀L,T,A. L ⊢ T ⁝ A → L ⊢ ⬊* T.
-#L #T #A #H
-@(acp_aaa … csn_acp csn_acr … H)
+theorem csn_aaa: ∀h,g,L,T,A. L ⊢ T ⁝ A → ⦃h, L⦄ ⊢ ⬊*[g] T.
+#h #g #L #T #A #H
+@(acp_aaa … (csn_acp h g) (csn_acr h g) … H)
 qed.