- the relocation properties of cpr are closed!

[helm.git] / matita / matita / contribs / lambda_delta / Basic_2 / unfold / ltpss.ma

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 4f2062a1456c9de7b69696ef18921a8e12de1d83..eb7803efe9631f72c282720ea9076685596aef24 100644 (file)
--- a/matita/matita/contribs/lambda_delta/Basic_2/unfold/ltpss.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/unfold/ltpss.ma
@@ -12,8 +12,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "Basic-2/substitution/ltps.ma".
-include "Basic-2/unfold/tpss.ma".
+include "Basic_2/substitution/ltps.ma".
+include "Basic_2/unfold/tpss.ma".
 
 (* PARTIAL UNFOLD ON LOCAL ENVIRONMENTS *************************************)
 
@@ -63,7 +63,7 @@ fact ltps_inv_atom2_aux: ∀d,e,L1,L2.
 ]
 qed.
 
-lemma drop_inv_atom2: ∀d,e,L1. L1 [d, e] ≫ ⋆ → L1 = ⋆.
+lemma ldrop_inv_atom2: ∀d,e,L1. L1 [d, e] ≫ ⋆ → L1 = ⋆.
 /2 width=5/ qed.
 
 fact ltps_inv_tps22_aux: ∀d,e,L1,L2. L1 [d, e] ≫ L2 → d = 0 → 0 < e →