update in ground_2 and 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 f24e507850a21470569138388286bcde62428fc5..096683f573a8076cbf70e5b635516d4ab5424979 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,6 +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 *)
 lemma frees_inv_drops_next: ∀f1,L1,T1. L1 ⊢ 𝐅*⦃T1⦄ ≡ f1 →
                             ∀I2,L2,V2,n. ⬇*[n] L1 ≡ L2.ⓑ{I2}V2 →
                             ∀g1. ⫯g1 = ⫱*[n] f1 →