xoa: change in naming convenctions for existential quantifies

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / unfold / tpss_tpss.ma

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 3f41b0083c12f81d75dfc662d6aa63ed04998644..d124bb32c806ff2c3d90c5d8ef8364827170db28 100644 (file)
--- 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.