X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_computation%2Flfsx_fqup.ma;h=e9879a17cc9e56609d6d2247d06aab8e2da800a4;hb=58ea181757dce19b875b2f5a224fe193b2263004;hp=10bcdd59c3d6e67619406786ce2b067150207806;hpb=670ad7822d59e598a38d9037d482d3de188b170c;p=helm.git

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 10bcdd59c..e9879a17c 100644
--- 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