X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frelocation%2Ffrees_weight.ma;h=04e8c370f07c7fd8f06d5275a52c878346791014;hb=50997cb3042073d58c2a16885ef0c82217367e63;hp=c8b3b7f466cfa111f0bd797f4ec8d62b61b3f958;hpb=560e9f41516968588e97bb6ff2049f85a425ac0a;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/frees_weight.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/frees_weight.ma
index c8b3b7f46..04e8c370f 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/frees_weight.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/frees_weight.ma
@@ -20,6 +20,7 @@ include "basic_2/relocation/frees.ma".
 
 (* Advanced properties ******************************************************)
 
+(* Notes: this replaces lemma 1400 concluding the "big tree" theorem *)
 lemma frees_total: ∀L,T. ∃f. L ⊢ 𝐅*⦃T⦄ ≡ f.
 @(f2_ind … rfw) #n #IH #L *
 [ cases L -L /3 width=2 by frees_atom, ex_intro/