some restyling ...

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / rt_computation / cpms_aaa.ma

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 08f2039c8bacd5fee9466f3f8eb72c61a83092c2..f4cc579aabcc11b9273201775c6ef5d7b9349853 100644 (file)
--- 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,8 +25,8 @@ 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):
-      ∀T. ⦃G, L⦄ ⊢ T ⁝ A → ∃U. ⦃G,L⦄ ⊢ T ➡*[n,h] U.
+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/
 | #n #IH #A #T1 #HT1 <plus_SO