update in binararies for λδ

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2A/grammar/lenv_weight.ma b/matita/matita/contribs/lambdadelta/basic_2A/grammar/lenv_weight.ma
index 598a9e31c829b2b1fa57c09b0f81c1c39da49521..02f9e30e756f97c7bb01634fbaeaf82cbdbf7d13 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2A/grammar/lenv_weight.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2A/grammar/lenv_weight.ma
@@ -28,7 +28,3 @@ interpretation "weight (local environment)" 'Weight L = (lw L).
 
 lemma lw_pair: ∀I,L,V. ♯{L} < ♯{L.ⓑ{I}V}.
 /3 width=1 by lt_plus_to_minus_r, monotonic_lt_plus_r/ qed.
-
-(* 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 *)