- context-sensitive computation: more properties

[helm.git] / matita / matita / contribs / lambda_delta / basic_2 / reducibility / cpr.ma

diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr.ma
index 220f8a648e19f02f1ee60555c497ccf57e137d15..fdbc9458fc00e636bf53c677803bf2a6f40559cc 100644 (file)
--- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr.ma
@@ -32,7 +32,7 @@ lemma cpr_intro: ∀L,T1,T,T2,d,e. T1 ➡ T → L ⊢ T [d, e] ▶* T2 → L ⊢
 /4 width=3/ qed-.
 
 (* Basic_1: was by definition: pr2_free *)
-lemma cpr_pr: ∀T1,T2. T1 ➡ T2 → ∀L. L ⊢ T1 ➡ T2.
+lemma cpr_tpr: ∀T1,T2. T1 ➡ T2 → ∀L. L ⊢ T1 ➡ T2.
 /2 width=3/ qed.
 
 lemma cpr_tpss: ∀L,T1,T2,d,e. L ⊢ T1 [d, e] ▶* T2 → L ⊢ T1 ➡ T2.