X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fstatic%2Fda_aaa.ma;h=c7903c24e4ba51dce66458f52c8e2860d2e900fa;hb=c60524dec7ace912c416a90d6b926bee8553250b;hp=7e9e4cc8873ca0780691d5e94f145d42042ffa1f;hpb=f10cfe417b6b8ec1c7ac85c6ecf5fb1b3fdf37db;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/da_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/static/da_aaa.ma
index 7e9e4cc88..c7903c24e 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/static/da_aaa.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/da_aaa.ma
@@ -19,7 +19,7 @@ include "basic_2/static/da.ma".
 
 (* Properties on atomic arity assignment for terms **************************)
 
-lemma aaa_da: ∀h,g,G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → ∃l. ⦃G, L⦄ ⊢ T ▪[h, g] l.
+lemma aaa_da: ∀h,g,G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → ∃d. ⦃G, L⦄ ⊢ T ▪[h, g] d.
 #h #g #G #L #T #A #H elim H -G -L -T -A
 [ #G #L #k elim (deg_total h g k) /3 width=2 by da_sort, ex_intro/
 | * #G #L #K #V #B #i #HLK #_ * /3 width=5 by da_ldef, da_ldec, ex_intro/