- support for atomic arities and candidates of reducibility started

[helm.git] / matita / matita / contribs / lambda_delta / Basic_2 / grammar / term.ma

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 f3f307cd62cdd9c41f09c789882a50c9a8f80104..42e7b8633a851ecc8e3bf93717455b62b5b3692a 100644 (file)
--- 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-.