X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Funwind%2Fsstas_ltpss_sn.ma;h=d066adb0db0b9977beb081cdd119b9f4d953e6fe;hb=08cb57944c0df08611d4f35d286e46c0d13e4813;hp=0a00fd9d861183ac72a3197660021376219579ed;hpb=9245402674a791dfdb943902f8288d742088c854;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/unwind/sstas_ltpss_sn.ma b/matita/matita/contribs/lambdadelta/basic_2/unwind/sstas_ltpss_sn.ma
index 0a00fd9d8..d066adb0d 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/unwind/sstas_ltpss_sn.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/unwind/sstas_ltpss_sn.ma
@@ -28,7 +28,7 @@ lapply (ltpss_sn_ltpssa … H) -H #H @(ltpssa_ind … H) -L2 /2 width=3/
 lapply (ltpssa_ltpss_sn … HL1) -HL1 #HL1
 lapply (ltpss_sn_dx_trans_eq … HL1 … HL2) -HL1 #HL12
 elim (IHL1 … H1) -IHL1 -H1 #U #HU1 #HTU
-elim (sstas_ltpss_dx_conf … HTU … HL2) -HTU -HL2 #U2 #H2 #HU2  
+elim (sstas_ltpss_dx_conf … HTU … HL2) -HTU -HL2 #U2 #H2 #HU2
 lapply (ltpss_sn_tpss_trans_eq … HU2 … HL12) -HU2 -HL12 #HU2
 lapply (tpss_trans_eq … HU1 HU2) -U /2 width=3/
 qed.