X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Funfold%2Ftpss_tpss.ma;fp=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Funfold%2Ftpss_tpss.ma;h=d124bb32c806ff2c3d90c5d8ef8364827170db28;hb=380ceb6b6552fd9ebd48d710ab12931d5d97e465;hp=3f41b0083c12f81d75dfc662d6aa63ed04998644;hpb=e8998d29ab83e7b6aa495a079193705b2f6743d3;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/tpss_tpss.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/tpss_tpss.ma
index 3f41b0083..d124bb32c 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/unfold/tpss_tpss.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/tpss_tpss.ma
@@ -56,7 +56,7 @@ lemma tpss_split_up: ∀L,T1,T2,d,e. L ⊢ T1 ▶* [d, e] T2 →
 | #T #T2 #_ #HT12 * #T3 #HT13 #HT3
   elim (tps_split_up … HT12 … Hdi Hide) -HT12 -Hide #T0 #HT0 #HT02
   elim (tpss_strap1_down … HT3 … HT0 ?) -T [2: >commutative_plus /2 width=1/ ]
-  /3 width=7 by ex2_1_intro, step/ (**) (* just /3 width=7/ is too slow *)
+  /3 width=7 by ex2_intro, step/ (**) (* just /3 width=7/ is too slow *)
 ]
 qed.