X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2FBasic_2%2Fsubstitution%2Fltps.ma;h=4f30025d31ce166d86fe2391364f4b0cbc9c7be5;hb=ef3bdc4be26f6518a82a79c64e986253f7aeaa3c;hp=c4b6c87f0c2831e38f632753e584d455278c3ea5;hpb=b5db76fe31ab35bae0257cb6684c511bcc531e45;p=helm.git

diff --git a/matita/matita/contribs/lambda_delta/Basic_2/substitution/ltps.ma b/matita/matita/contribs/lambda_delta/Basic_2/substitution/ltps.ma
index c4b6c87f0..4f30025d3 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/substitution/ltps.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/substitution/ltps.ma
@@ -179,9 +179,9 @@ lemma ltps_inv_tps12: ∀L1,K2,I,V2,d,e. L1 [d, e] ▶ K2. ⓑ{I} V2 → 0 < d 
 /2 width=3/ qed-.
 
 (* Basic_1: removed theorems 27:
-            csubst0_clear_O csubst0_ldrop_lt csubst0_ldrop_gt csubst0_ldrop_eq
+            csubst0_clear_O csubst0_drop_lt csubst0_drop_gt csubst0_drop_eq
             csubst0_clear_O_back csubst0_clear_S csubst0_clear_trans
-            csubst0_ldrop_gt_back csubst0_ldrop_eq_back csubst0_ldrop_lt_back
+            csubst0_drop_gt_back csubst0_drop_eq_back csubst0_drop_lt_back
             csubst0_gen_sort csubst0_gen_head csubst0_getl_ge csubst0_getl_lt
             csubst0_gen_S_bind_2 csubst0_getl_ge_back csubst0_getl_lt_back
             csubst0_snd_bind csubst0_fst_bind csubst0_both_bind