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

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 e1214dbac..306766f42 100644
--- 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-.