X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_computation%2Fcpmre_aaa.ma;h=8639ec1a37f70f4d9696dd1e31ba7fa88da10f7a;hp=3f3cf8bffc23ea37ca288739c9f603e093116329;hb=3c7b4071a9ac096b02334c1d47468776b948e2de;hpb=2f6f2b7c01d47d23f61dd48d767bcb37aecdcfea

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpmre_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpmre_aaa.ma
index 3f3cf8bff..8639ec1a3 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpmre_aaa.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpmre_aaa.ma
@@ -27,6 +27,6 @@ lemma cpmre_total_aaa (h) (n) (A) (G) (L):
 elim (cpms_total_aaa h … n … HT1) #T0 #HT10
 elim (cprre_total_csx h G L T0)
 [ #T2 /3 width=4 by cpms_cprre_trans, ex_intro/
-| /4 width=4 by cpms_fwd_cpxs, aaa_csx, csx_cpxs_trans/
+| /4 width=5 by cpms_fwd_cpxs, aaa_csx, csx_cpxs_trans/
 ]
 qed-.