X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fstatic%2Ffrees_drops.ma;h=096683f573a8076cbf70e5b635516d4ab5424979;hb=a5c71699f1d0cf63a769c71dd8b8cd5dfff1933d;hp=f24e507850a21470569138388286bcde62428fc5;hpb=02128ad2d07f4763e311a7f449d87aa022014c1f;p=helm.git

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 f24e50785..096683f57 100644
--- 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 →