X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Funfold%2Fltpss_sn_alt.ma;h=8b414d2030b401f9f8b88c727c1aeac57492bd3e;hb=380ceb6b6552fd9ebd48d710ab12931d5d97e465;hp=7a453d270097fd12a7aec7a2c5444baa92832167;hpb=e8998d29ab83e7b6aa495a079193705b2f6743d3;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_sn_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_sn_alt.ma
index 7a453d270..8b414d203 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_sn_alt.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_sn_alt.ma
@@ -106,7 +106,7 @@ lemma ltpss_sn_strip: ∀L0,L1,d1,e1. L0 ⊢ ▶* [d1, e1] L1 →
 #L0 #L1 #d1 #e1 #H #L2 #d2 #e2 #HL02
 lapply (ltpss_sn_ltpssa … H) -H #HL01
 elim (ltpssa_strip … HL01 … HL02) -L0
-/3 width=3 by ltpssa_ltpss_sn, ex2_1_intro/
+/3 width=3 by ltpssa_ltpss_sn, ex2_intro/
 qed.
 
 (* Note: this should go in ltpss_sn_ltpss_sn.ma *)
@@ -152,5 +152,5 @@ theorem ltpss_sn_conf: ∀L0,L1,d1,e1. L0 ⊢ ▶* [d1, e1] L1 →
 lapply (ltpss_sn_ltpssa … H1) -H1 #HL01
 lapply (ltpss_sn_ltpssa … H2) -H2 #HL02
 elim (ltpssa_conf … HL01 … HL02) -L0
-/3 width=3 by ltpssa_ltpss_sn, ex2_1_intro/
+/3 width=3 by ltpssa_ltpss_sn, ex2_intro/
 qed.