X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Funfold%2Fgr2_plus.ma;h=82366bc72cbc7661fda759a3afeafab671b304cd;hb=08cb57944c0df08611d4f35d286e46c0d13e4813;hp=bd8d1a9be416f9203208d8505408c1a116a2629d;hpb=9245402674a791dfdb943902f8288d742088c854;p=helm.git

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 bd8d1a9be..82366bc72 100644
--- 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-.