X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fstatic%2Ffrees_drops.ma;h=fe24eadf5d0496b0dce3a9145e2e441f55e4174b;hp=75e69391232a270f04f2b9a672628032026ead4f;hb=222044da28742b24584549ba86b1805a87def070;hpb=397413c4196f84c81d61ba7dd79b54ab1c428ebb

diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/frees_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/static/frees_drops.ma
index 75e693912..fe24eadf5 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/static/frees_drops.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/frees_drops.ma
@@ -191,7 +191,7 @@ lemma frees_inv_lifts: ∀b,f2,L,U. L ⊢ 𝐅*⦃U⦄ ≘ f2 →
 /3 width=7 by frees_eq_repl_back, coafter_inj/
 qed-.
 
-(* Note: this is used by lfxs_conf and might be modified *)
+(* Note: this is used by rex_conf and might be modified *)
 lemma frees_inv_drops_next: ∀f1,L1,T1. L1 ⊢ 𝐅*⦃T1⦄ ≘ f1 →
                             ∀I2,L2,V2,n. ⬇*[n] L1 ≘ L2.ⓑ{I2}V2 →
                             ∀g1. ↑g1 = ⫱*[n] f1 →