X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Funfold%2Fltpss_sn_ldrop.ma;h=bc4d73f3e35b4ca1cf9feaf6e151229bba850516;hb=8ff4315142253a1a0478b67c07dddf70c36f50cd;hp=dda41e4c30b72e3938d59ae95394ac71928e1cc9;hpb=18df696e2c97546e5d42e86d18691b8546339160;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_sn_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_sn_ldrop.ma
index dda41e4c3..bc4d73f3e 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_sn_ldrop.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_sn_ldrop.ma
@@ -133,7 +133,7 @@ qed.
 
 lemma ldrop_ltpss_sn_trans_be: ∀L1,K1,d1,e1. ⇩[d1, e1] L1 ≡ K1 →
                                ∀K2,d2,e2. K1 ⊢ ▶* [d2, e2] K2 →
-                               d2 ≤ d1 → d1 ≤ d2 + e2 → 
+                               d2 ≤ d1 → d1 ≤ d2 + e2 →
                                ∃∃L2. L1 ⊢ ▶* [d2, e1 + e2] L2 &
                                      ⇩[d1, e1] L2 ≡ K2.
 #L1 #K1 #d1 #e1 #H elim H -L1 -K1 -d1 -e1