- lambdadelta: last recursive part of preservation finally proved!

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

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 dda41e4c30b72e3938d59ae95394ac71928e1cc9..bc4d73f3e35b4ca1cf9feaf6e151229bba850516 100644 (file)
--- 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