decentralized notation in lambda

[helm.git] / matita / matita / contribs / lambdadelta / static_2 / syntax / tweq_teqx.ma

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 1d29c33aa24856177bb4d3e671557c61ccf24822..39cf1e3538800bcdfb3c3ad3d0073f254664b3da 100644 (file)
--- 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/