X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fstatic%2Ffrees.ma;h=3699063ce1ef280c3e1afddcc64a28015bac12e7;hb=f4e73c50acfc4ed453edd423c9bbe28af5dc9c4c;hp=31bf511d395c83b0635b867802f1e8c34f20c501;hpb=926796df5884453d8f0cf9f294d7776d469ef45b;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/frees.ma b/matita/matita/contribs/lambdadelta/basic_2/static/frees.ma
index 31bf511d3..3699063ce 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/static/frees.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/frees.ma
@@ -185,13 +185,14 @@ lemma frees_gref_gen: ∀f,L,p. 𝐈⦃f⦄ → L ⊢ 𝐅*⦃§p⦄ ≡ f.
 /4 width=3 by frees_eq_repl_back, frees_gref, frees_atom, eq_push_inv_isid/
 qed.
 
-(* Basic_2A1: removed theorems 27:
+(* Basic_2A1: removed theorems 30:
               frees_eq frees_be frees_inv
               frees_inv_sort frees_inv_gref frees_inv_lref frees_inv_lref_free
               frees_inv_lref_skip frees_inv_lref_ge frees_inv_lref_lt
               frees_inv_bind frees_inv_flat frees_inv_bind_O
               frees_lref_eq frees_lref_be frees_weak
               frees_bind_sn frees_bind_dx frees_flat_sn frees_flat_dx
+              frees_lift_ge frees_inv_lift_be frees_inv_lift_ge 
               lreq_frees_trans frees_lreq_conf
               llor_atom llor_skip llor_total
               llor_tail_frees llor_tail_cofrees