- more properties on strongly normalizing terms

[helm.git] / matita / matita / contribs / lambda_delta / Basic_2 / reducibility / ltpr_ldrop.ma

diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/ltpr_ldrop.ma b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/ltpr_ldrop.ma
index 5c725a948508bdc620f0a5dd8be197f737e3ff1b..090e8cfbf7c1be444d53f4b7327e6ae7d7187851 100644 (file)
--- a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/ltpr_ldrop.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/ltpr_ldrop.ma
@@ -17,7 +17,7 @@ include "Basic_2/reducibility/ltpr.ma".
 
 (* CONTEXT-FREE PARALLEL REDUCTION ON LOCAL ENVIRONMENTS ********************)
 
-(* Basic_1: was: wcpr0_ldrop *)
+(* Basic_1: was: wcpr0_drop *)
 lemma ltpr_ldrop_conf: ∀L1,K1,d,e. ⇩[d, e] L1 ≡ K1 → ∀L2. L1 ➡ L2 →
                        ∃∃K2. ⇩[d, e] L2 ≡ K2 & K1 ➡ K2.
 #L1 #K1 #d #e #H elim H -L1 -K1 -d -e
@@ -34,7 +34,7 @@ lemma ltpr_ldrop_conf: ∀L1,K1,d,e. ⇩[d, e] L1 ≡ K1 → ∀L2. L1 ➡ L2 
 ]
 qed.
 
-(* Basic_1: was: wcpr0_ldrop_back *)
+(* Basic_1: was: wcpr0_drop_back *)
 lemma ldrop_ltpr_trans: ∀L1,K1,d,e. ⇩[d, e] L1 ≡ K1 → ∀K2. K1 ➡ K2 →
                         ∃∃L2. ⇩[d, e] L2 ≡ K2 & L1 ➡ L2.
 #L1 #K1 #d #e #H elim H -L1 -K1 -d -e