X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_computation%2Fcpre_cpms.ma;fp=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_computation%2Fcpre_cpms.ma;h=2dd997c4582798197a2e1b184a70ecd4aa6d648f;hb=c0d38a82464481e3c8fd68e4b00d7b9b448df462;hp=a6fc27e18e026977006c2e0d0e4abf8c747bf851;hpb=0fea4ed429678c3293027cfe76fdbe15cfa331cb;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpre_cpms.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpre_cpms.ma
index a6fc27e18..2dd997c45 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpre_cpms.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpre_cpms.ma
@@ -23,5 +23,5 @@ lemma cpms_cpre_trans (h) (n) (G) (L):
       ∀T1,T0. ⦃G,L⦄ ⊢T1 ➡*[n,h] T0 →
       ∀T2. ⦃G,L⦄ ⊢ T0 ➡*[h] 𝐍⦃T2⦄ → ⦃G,L⦄ ⊢ T1 ➡*[h,n] 𝐍⦃T2⦄.
 #h #n #G #L #T1 #T0 #HT10 #T2 * #HT02 #HT2
-/3 width=3 by cpms_cprs_trans, conj/
+/3 width=3 by cpms_cprs_trans, cpme_intro/
 qed-.