- improved Makefile esp. with the "trim" function

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/gr2_plus.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/gr2_plus.ma
index bd8d1a9be416f9203208d8505408c1a116a2629d..82366bc72cbc7661fda759a3afeafab671b304cd 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/unfold/gr2_plus.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/gr2_plus.ma
@@ -35,6 +35,6 @@ lemma pluss_inv_cons2: ∀i,d,e,des2,des. des + i = {d, e} @ des2 →
                        ∃∃des1. des1 + i = des2 & des = {d - i, e} @ des1.
 #i #d #e #des2 * normalize
 [ #H destruct
-| #d1 #e1 #des1 #H destruct /2 width=3/ 
+| #d1 #e1 #des1 #H destruct /2 width=3/
 ]
 qed-.