X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_computation%2Fcpms_aaa.ma;h=41d1340805b23398a4d448c448224fce0cd020cc;hp=08f2039c8bacd5fee9466f3f8eb72c61a83092c2;hb=bf2b1df641df98a3b614a8c3d53edee8beb0964a;hpb=dd93a0919b67bead0d4f07d49dfc198006edc9aa

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_aaa.ma
index 08f2039c8..41d134080 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_aaa.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_aaa.ma
@@ -25,7 +25,7 @@ include "basic_2/rt_computation/cpms_cpxs.ma".
 lemma cpms_aaa_conf (n) (h): ∀G,L. Conf3 … (aaa G L) (cpms h G L n).
 /3 width=5 by cpms_fwd_cpxs, cpxs_aaa_conf/ qed-.
 
-lemma aaa_cpms_total (h) (G) (L) (n) (A):
+lemma cpms_total_aaa (h) (G) (L) (n) (A):
       ∀T. ⦃G, L⦄ ⊢ T ⁝ A → ∃U. ⦃G,L⦄ ⊢ T ➡*[n,h] U.
 #h #G #L #n elim n -n
 [ /2 width=3 by ex_intro/