X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fcomputation%2Fcprs.ma;h=c0e440d69bbc70c80b488ebb4f461139582c4780;hb=f62eeb3c7824564ccbe4fff6e75ddee46ca39cc0;hp=1b3bcf66638c0246bb4c8137a78fc70ade583171;hpb=ef49e0e7f5f298c299afdd3cbfdc2404ecb93879;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs.ma
index 1b3bcf666..c0e440d69 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs.ma
@@ -66,8 +66,8 @@ lemma cprs_cpss_trans: ∀L,T1,T. L ⊢ T1 ➡* T → ∀T2. L ⊢ T ▶* T2 →
 lemma cpss_cprs_trans: ∀L,T1,T. L ⊢ T1 ▶* T → ∀T2. L ⊢ T ➡* T2 → L ⊢ T1 ➡* T2.
 /3 width=3/ qed-.
 
-lemma cprs_lsubr_trans: lsubr_trans … cprs.
-/3 width=3 by cpr_lsubr_trans, TC_lsubr_trans/
+lemma cprs_lsubr_trans: lsub_trans … cprs lsubr.
+/3 width=5 by cpr_lsubr_trans, TC_lsub_trans/
 qed-.
 
 (* Basic_1: was: pr3_pr1 *)