X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Funfold%2Fltpss_dx_tpss.ma;h=04af50c8c172c04af2a40fe313fb7dde6a7d82d0;hb=08cb57944c0df08611d4f35d286e46c0d13e4813;hp=c3840c31ca5b32230df38f1869a316b715799bde;hpb=9245402674a791dfdb943902f8288d742088c854;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_dx_tpss.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_dx_tpss.ma
index c3840c31c..04af50c8c 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_dx_tpss.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_dx_tpss.ma
@@ -59,7 +59,7 @@ lemma ltpss_dx_tps_conf: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 ▶ [d2, e2] U2 →
   elim (IHTU2 … HL01) -IHTU2 -HL01 /3 width=5/
 ]
 qed.
-  
+
 lemma ltpss_dx_tpss_trans_ge: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 ▶* [d2, e2] U2 →
                               ∀L1,d1,e1. L1 ▶* [d1, e1] L0 → d1 + e1 ≤ d2 →
                               L1 ⊢ T2 ▶* [d2, e2] U2.