milestone update in basic_2, update in ground and static_2

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

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 3f3cf8bffc23ea37ca288739c9f603e093116329..8639ec1a37f70f4d9696dd1e31ba7fa88da10f7a 100644 (file)
--- 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-.