X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_transition%2Flfpx_aaa.ma;h=8c5fc717f1f831d70ac13a9eb1c15901afb11b51;hb=d4ab51c20dbccd1e88cd2c4dcdaf3b4e56301155;hp=bc6e8a43ab0522bf1ea62fe6e1981a8594997367;hpb=d1bd9d230123f4045e2472d073c5dc4b5da30b34;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_aaa.ma
index bc6e8a43a..8c5fc717f 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_aaa.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_aaa.ma
@@ -73,10 +73,9 @@ lemma cpx_aaa_conf_lfpx: ∀h,G,L1,T1,A. ⦃G, L1⦄ ⊢ T1 ⁝ A →
 ]
 qed-.
 
-lemma cpx_aaa_conf: ∀h,G,L,T1,A. ⦃G, L⦄ ⊢ T1 ⁝ A →
-                    ∀T2. ⦃G, L⦄ ⊢ T1 ⬈[h] T2 → ⦃G, L⦄ ⊢ T2 ⁝ A.
+lemma cpx_aaa_conf: ∀h,G,L. Conf3 … (aaa G L) (cpx h G L).
 /2 width=6 by cpx_aaa_conf_lfpx/ qed-.
 
-lemma lfpx_aaa_conf: ∀h,G,L1,T,A. ⦃G, L1⦄ ⊢ T ⁝ A →
-                     ∀L2. ⦃G, L1⦄ ⊢ ⬈[h, T] L2 → ⦃G, L2⦄ ⊢ T ⁝ A.
+(* Basic_2A1: uses: lpx_aaa_conf *)
+lemma lfpx_aaa_conf: ∀h,G,T. Conf3 … (λL. aaa G L T) (lfpx h G T).
 /2 width=6 by cpx_aaa_conf_lfpx/ qed-.