X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fstatic_2%2Fsyntax%2Ftweq_teqx.ma;h=39cf1e3538800bcdfb3c3ad3d0073f254664b3da;hb=613d8642b1154dde0c026cbdcd96568910198251;hp=1d29c33aa24856177bb4d3e671557c61ccf24822;hpb=adb9ba187619cea977d1d22971eba27eb437cd6a;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/tweq_teqx.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/tweq_teqx.ma
index 1d29c33aa..39cf1e353 100644
--- a/matita/matita/contribs/lambdadelta/static_2/syntax/tweq_teqx.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/syntax/tweq_teqx.ma
@@ -24,7 +24,7 @@ lemma teqx_tweq: ∀T1,T2. T1 ≛ T2 → T1 ≅ T2.
 [ /1 width=1 by tweq_sort/
 | /1 width=1 by tweq_lref/
 | /1 width=1 by tweq_gref/
-| cases p -p /2 width=1 by tweq_abbr_pos, tweq_abbr_neg/  
+| cases p -p /2 width=1 by tweq_abbr_pos, tweq_abbr_neg/
 | /1 width=1 by tweq_abst/
 | /2 width=1 by tweq_appl/
 | /2 width=1 by tweq_cast/