X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fstatic%2Fssta_ltpss_dx.ma;h=48ac6a400ca6a753fc8d72abbecaa8d630dd6aea;hb=08cb57944c0df08611d4f35d286e46c0d13e4813;hp=ccc9ecc9d3214a785c419b8c5579aaf54bdef9a5;hpb=9245402674a791dfdb943902f8288d742088c854;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/ssta_ltpss_dx.ma b/matita/matita/contribs/lambdadelta/basic_2/static/ssta_ltpss_dx.ma
index ccc9ecc9d..48ac6a400 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/static/ssta_ltpss_dx.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/ssta_ltpss_dx.ma
@@ -106,7 +106,7 @@ lemma ssta_ltpss_dx_tps_conf: ∀h,g,L1,T1,U1,l. ⦃h, L1⦄ ⊢ T1 •[g, l] U1
                               ∀L2,d,e. L1 ▶* [d, e] L2 →
                               ∀T2. L2 ⊢ T1 ▶ [d, e] T2 →
                               ∃∃U2. ⦃h, L2⦄ ⊢ T2 •[g, l] U2 &
-			            L2 ⊢ U1 ▶* [d, e] U2.
+                                    L2 ⊢ U1 ▶* [d, e] U2.
 /3 width=5/ qed.
 
 lemma ssta_ltpss_dx_conf: ∀h,g,L1,T,U1,l. ⦃h, L1⦄ ⊢ T •[g, l] U1 →