- lambda_delta: morew propertie in context-sensitive computation

[helm.git] / matita / matita / contribs / lambda_delta / Basic_2 / computation / cprs_cprs.ma

diff --git a/matita/matita/contribs/lambda_delta/Basic_2/computation/cprs_cprs.ma b/matita/matita/contribs/lambda_delta/Basic_2/computation/cprs_cprs.ma
index 54a94b4963361270c066bc1facbae589db31130b..16c1a6256164a873d0b3c143a4d6b32163d2459e 100644 (file)
--- a/matita/matita/contribs/lambda_delta/Basic_2/computation/cprs_cprs.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/computation/cprs_cprs.ma
@@ -82,7 +82,7 @@ lemma cprs_flat: ∀I,L,T1,T2. L ⊢ T1 ➡* T2 → ∀V1,V2. L ⊢ V1 ➡* V2 
 @(cprs_trans … IHV1) -IHV1 /2 width=1/ 
 qed.
 
-(* Basic_1: was only: pr3_pr2_pr3_t *)
+(* Basic_1: was only: pr3_pr2_pr3_t pr3_wcpr0_t *)
 lemma lcpr_cprs_trans: ∀L1,L2. L1 ⊢ ➡ L2 →
                        ∀T1,T2. L2 ⊢ T1 ➡* T2 → L1 ⊢ T1 ➡* T2.
 #L1 #L2 #HL12 #T1 #T2 #H @(cprs_ind … H) -T2 //