X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fstatic%2Flfdeq.ma;h=f6bc891d7af225ef58240b517c592bdf69f83728;hb=670ad7822d59e598a38d9037d482d3de188b170c;hp=aa6484ace27b98d058aba586a2af2dca2a3630d8;hpb=7412538ab43afe9a19c5f4be369bed82b2ab6193;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq.ma
index aa6484ace..f6bc891d7 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq.ma
@@ -176,11 +176,12 @@ lemma lfdeq_fwd_dx: ∀h,o,I,L1,K2,V2. ∀T:term. L1 ≡[h, o, T] K2.ⓑ{I}V2 
                     ∃∃K1,V1. L1 = K1.ⓑ{I}V1.
 /2 width=5 by lfxs_fwd_dx/ qed-.
 
-(* Basic_2A1: removed theorems 30: 
+(* Basic_2A1: removed theorems 31: 
               lleq_ind lleq_inv_bind lleq_inv_flat lleq_fwd_length lleq_fwd_lref
               lleq_fwd_drop_sn lleq_fwd_drop_dx
               lleq_fwd_bind_sn lleq_fwd_bind_dx lleq_fwd_flat_sn lleq_fwd_flat_dx
               lleq_sort lleq_skip lleq_lref lleq_free lleq_gref lleq_bind lleq_flat
               lleq_refl lleq_Y lleq_sym lleq_ge_up lleq_ge lleq_bind_O llpx_sn_lrefl
               lleq_trans lleq_canc_sn lleq_canc_dx lleq_nlleq_trans nlleq_lleq_div
+              lleq_dec 
 *)