update in basic_2 and apps_2

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / rt_transition / lpr_aaa.ma

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 c051cf6d9d6f778b3bb3faedb16e14ceadd3696a..2e6e577ef85c0bfcf75d3b9df236bcd20aabf656 100644 (file)
--- 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-.