X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2Fbasic_2%2Funfold%2Fltpss.ma;h=89b19ea4576c8505f730d3c3115ab38e429edcd6;hb=439b6ec33d749ba4e6ae0938e973a85bc23e306e;hp=169f0e276e0e680acdc8d8260dbb231caa741048;hpb=78d4844bcccb3deb58a3179151c3045298782b18;p=helm.git

diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss.ma
index 169f0e276..89b19ea45 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss.ma
@@ -219,7 +219,7 @@ lemma ltpss_inv_tpss12: ∀L1,K2,I,V2,d,e. L1 ▶* [d, e] K2. ⓑ{I} V2 → 0 <
                                  L1 = K1. ⓑ{I} V1.
 /2 width=3/ qed-.
 
-(* Basic_1: removed theorems 27:
+(* Basic_1: removed theorems 28:
             csubst0_clear_O csubst0_drop_lt csubst0_drop_gt csubst0_drop_eq
             csubst0_clear_O_back csubst0_clear_S csubst0_clear_trans
             csubst0_drop_gt_back csubst0_drop_eq_back csubst0_drop_lt_back
@@ -228,5 +228,5 @@ lemma ltpss_inv_tpss12: ∀L1,K2,I,V2,d,e. L1 ▶* [d, e] K2. ⓑ{I} V2 → 0 <
             csubst0_snd_bind csubst0_fst_bind csubst0_both_bind
             csubst1_head csubst1_flat csubst1_gen_head
             csubst1_getl_ge csubst1_getl_lt csubst1_getl_ge_back getl_csubst1
-
+            fsubst0_gen_base
 *)