- improved Makefile esp. with the "trim" function

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / unfold / ltpss_dx_tpss.ma

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 c3840c31ca5b32230df38f1869a316b715799bde..04af50c8c172c04af2a40fe313fb7dde6a7d82d0 100644 (file)
--- 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.