X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fgrammar%2Flenv_weight.ma;fp=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fgrammar%2Flenv_weight.ma;h=642a3d1b84f3af6a7fe4f36d3a7fd0eb77ae8a3d;hb=ac7479f9a292448d12761da4345d668d74b8d308;hp=7893bff32ce58267bcbf267af192c8ce8b891884;hpb=8910c1dc3fcc1da950d0c71f0f1a0150c5557520;p=helm.git diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_weight.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_weight.ma index 7893bff32..642a3d1b8 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_weight.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_weight.ma @@ -29,5 +29,6 @@ interpretation "weight (local environment)" 'Weight L = (lw L). lemma lw_pair: ∀I,L,V. ♯{L} < ♯{L.ⓑ{I}V}. /3 width=1/ qed. -(* Basic_1: removed theorems 2: clt_cong clt_head clt_thead *) +(* Basic_1: removed theorems 4: clt_cong clt_head clt_thead clt_wf_ind *) +(* Basic_1: removed local theorems 1: clt_wf__q_ind *) (* Basic_1: note: clt_thead should be renamed clt_ctail *)