milestone in basic_2

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / rt_computation / cpre_cpms.ma

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 a6fc27e18e026977006c2e0d0e4abf8c747bf851..2dd997c4582798197a2e1b184a70ecd4aa6d648f 100644 (file)
--- 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-.