renaming in basic_2

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / static / frees_drops.ma

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 75e69391232a270f04f2b9a672628032026ead4f..fe24eadf5d0496b0dce3a9145e2e441f55e4174b 100644 (file)
--- 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 →