X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_transition%2Flpr_aaa.ma;h=2e6e577ef85c0bfcf75d3b9df236bcd20aabf656;hp=c051cf6d9d6f778b3bb3faedb16e14ceadd3696a;hb=ca7327c20c6031829fade8bb84a3a1bb66113f54;hpb=25c634037771dff0138e5e8e3d4378183ff49b86

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lpr_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lpr_aaa.ma
index c051cf6d9..2e6e577ef 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lpr_aaa.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lpr_aaa.ma
@@ -19,5 +19,5 @@ include "basic_2/rt_transition/lpx_aaa.ma".
 
 (* Properties with atomic arity assignment for terms ************************)
 
-lemma lpr_aaa_conf (h): ∀G,T. Conf3 … (λL. aaa G L T) (lpr h G).
+lemma lpr_aaa_conf (h): ∀G,T. Conf3 … (λL. aaa G L T) (lpr h 0 G).
 /3 width=5 by lpx_aaa_conf, lpr_fwd_lpx/ qed-.