the newly generated web pages ...

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / relocation / frees_weight.ma

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 c8b3b7f466cfa111f0bd797f4ec8d62b61b3f958..04e8c370f07c7fd8f06d5275a52c878346791014 100644 (file)
--- 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/