- improved Makefile esp. with the "trim" function

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / unwind / sstas_ltpss_sn.ma

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 0a00fd9d861183ac72a3197660021376219579ed..d066adb0db0b9977beb081cdd119b9f4d953e6fe 100644 (file)
--- 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.