update in basic_2 and apps_2

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs_aaa.ma
index e1214dbac5a6b968f260f70a996f02ed7e194331..306766f42b0be6be2643229133e6c78620ce5ffc 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs_aaa.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs_aaa.ma
@@ -19,5 +19,6 @@ include "basic_2/rt_computation/lprs_lpxs.ma".
 
 (* Properties with atomic arity assignment for terms ************************)
 
-lemma lprs_aaa_conf (h) (G) (T): Conf3 … (λL. aaa G L T) (lprs h G).
+lemma lprs_aaa_conf (h) (G) (T):
+      Conf3 … (λL. aaa G L T) (lprs h 0 G).
 /3 width=5 by lprs_fwd_lpxs, lpxs_aaa_conf/ qed-.