- "big tree" order implemented

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / grammar / lenv_weight.ma

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 7893bff32ce58267bcbf267af192c8ce8b891884..642a3d1b84f3af6a7fe4f36d3a7fd0eb77ae8a3d 100644 (file)
--- 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 *)