X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2FBasic_2%2Fgrammar%2Fterm.ma;h=42e7b8633a851ecc8e3bf93717455b62b5b3692a;hb=9aa9a54946719d3fdb4cadb7c7d33fd13956c083;hp=f3f307cd62cdd9c41f09c789882a50c9a8f80104;hpb=18ac3a120a3887b144c1d0e13d64d6e1c2d10d93;p=helm.git

diff --git a/matita/matita/contribs/lambda_delta/Basic_2/grammar/term.ma b/matita/matita/contribs/lambda_delta/Basic_2/grammar/term.ma
index f3f307cd6..42e7b8633 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/grammar/term.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/grammar/term.ma
@@ -43,7 +43,7 @@ lemma discr_tpair_xy_x: ∀I,T,V. 𝕔{I} V. T = V → False.
 [ #J #H destruct
 | #J #W #U #IHW #_ #H destruct
   -H >e0 in e1; normalize (**) (* destruct: one quality is not simplified, the destucted equality is not erased *)
-  /2 width=1/ 
+  /2 width=1/
 ]
 qed-.