- lfpxs based on tc_lfxs

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

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 2f90bf27e8b9011a7e4c0509b655cbf03d0d1ee1..bc6e8a43ab0522bf1ea62fe6e1981a8594997367 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_aaa.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_aaa.ma
@@ -21,7 +21,7 @@ include "basic_2/rt_transition/lfpx_fqup.ma".
 (* Properties with atomic arity assignment for terms ************************)
 
 (* Note: lemma 500 *)
-(* Basic_2A1: was: cpx_lpx_aaa_conf *)
+(* Basic_2A1: uses: cpx_lpx_aaa_conf *)
 lemma cpx_aaa_conf_lfpx: ∀h,G,L1,T1,A. ⦃G, L1⦄ ⊢ T1 ⁝ A →
                          ∀T2. ⦃G, L1⦄ ⊢ T1 ⬈[h] T2 →
                          ∀L2. ⦃G, L1⦄ ⊢ ⬈[h, T1] L2 → ⦃G, L2⦄ ⊢ T2 ⁝ A.