X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fstatic%2Ffrees_fqup.ma;h=c82690309a7b312ebb4e44ce193c4fac0adf41a3;hb=199ba569adf94f9948053352c2c0a1c6deb62bc5;hp=797e4f3240fec5a2a225c91b9005366ed1db4cb8;hpb=c4c23fb49f67e69b3193fc8233339f6ca016a8e9;p=helm.git diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/frees_fqup.ma b/matita/matita/contribs/lambdadelta/basic_2/static/frees_fqup.ma index 797e4f324..c82690309 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/frees_fqup.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/frees_fqup.ma @@ -19,7 +19,7 @@ include "basic_2/static/frees.ma". (* Advanced properties ******************************************************) -(* Notes: this replaces lemma 1400 concluding the "big tree" theorem *) +(* Note: this replaces lemma 1400 concluding the "big tree" theorem *) lemma frees_total: ∀L,T. ∃f. L ⊢ 𝐅*⦃T⦄ ≡ f. #L #T @(fqup_wf_ind_eq … (⋆) L T) -L -T #G0 #L0 #T0 #IH #G #L *