update in basic_2

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_aaa.ma
index 899bfc1cfc8c62f78000fecd150207d51d5cd325..d3dd5dd0de240a10903119520b2968002659f802 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_aaa.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_aaa.ma
@@ -19,7 +19,7 @@ include "basic_2/rt_transition/lfpr_lfpx.ma".
 
 (* Properties with atomic arity assignment for terms ************************)
 
-lemma cpr_aaa_conf: ∀h,G,L. Conf3 … (aaa G L) (cpm 0 h G L).
+lemma cpr_aaa_conf: ∀h,G,L. Conf3 … (aaa G L) (cpm h G L 0).
 /3 width=5 by cpx_aaa_conf, cpm_fwd_cpx/ qed-.
 
 (* Basic_2A1: uses: lpr_aaa_conf *)