- lfpxs based on tc_lfxs

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_fqup.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_fqup.ma
index 10bcdd59c3d6e67619406786ce2b067150207806..e9879a17cc9e56609d6d2247d06aab8e2da800a4 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_fqup.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_fqup.ma
@@ -19,7 +19,7 @@ include "basic_2/rt_computation/lfsx.ma".
 
 (* Advanced properties ******************************************************)
 
-(* Basic_2A1: was: lsx_atom *)
+(* Basic_2A1: uses: lsx_atom *)
 lemma lfsx_atom: ∀h,o,G,T. G ⊢ ⬈*[h, o, T] 𝐒⦃⋆⦄.
 #h #o #G #T @lfsx_intro
 #Y #H #HI lapply (lfpx_inv_atom_sn … H) -H