- improved Makefile esp. with the "trim" function

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/delift_ltpss.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/delift_ltpss.ma
index a0ac3cf479fbcb2c89c66dda8b8e4deb4ceaffc8..2954223480cfa1c4ba04e04ea9b99671465aae64 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/unfold/delift_ltpss.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/delift_ltpss.ma
@@ -28,6 +28,6 @@ qed.
 
 lemma ltpss_sn_delift_trans_eq: ∀L,K,d,e. L ⊢ ▶* [d, e] K →
                                 ∀T1,T2. K ⊢ ▼*[d, e] T1 ≡ T2 → L ⊢ ▼*[d, e] T1 ≡ T2.
-#L #K #d #e #HLK #T1 #T2 * #T #HT1 #HT2 
+#L #K #d #e #HLK #T1 #T2 * #T #HT1 #HT2
 lapply (ltpss_sn_tpss_trans_eq … HT1 … HLK) -K /2 width=3/
 qed.