X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2A%2Fgrammar%2Flenv_weight.ma;h=02f9e30e756f97c7bb01634fbaeaf82cbdbf7d13;hp=598a9e31c829b2b1fa57c09b0f81c1c39da49521;hb=2f6f2b7c01d47d23f61dd48d767bcb37aecdcfea;hpb=3a4509b8e569181979f5b15808361c83eb1ae49a 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 598a9e31c..02f9e30e7 100644 --- 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 *)