- some renaming according to the written version of basic_2

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

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 7e9e4cc8873ca0780691d5e94f145d42042ffa1f..c7903c24e4ba51dce66458f52c8e2860d2e900fa 100644 (file)
--- 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/