SubstTactic: bug fix

[helm.git] / helm / software / matita / contribs / RELATIONAL / NPlus / monoid.ma

diff --git a/helm/software/matita/contribs/RELATIONAL/NPlus/monoid.ma b/helm/software/matita/contribs/RELATIONAL/NPlus/monoid.ma
index a7d56eeb3e2f1e4ddf9bdd1672747bc6641eb0de..4d1705b90da0d1eba00f5e98cd5958c2fc639344 100644 (file)
--- a/helm/software/matita/contribs/RELATIONAL/NPlus/monoid.ma
+++ b/helm/software/matita/contribs/RELATIONAL/NPlus/monoid.ma
@@ -22,7 +22,7 @@ theorem nplus_zero_1: \forall q. zero + q == q.
  intros. elim q; clear q; auto.
 qed.
 
-theorem nplus_succ_1: \forall p,q,r. NPlus p q r \to 
+theorem nplus_succ_1: \forall p,q,r. (p + q == r) \to 
                       (succ p) + q == (succ r).
  intros. elim H; clear H q r; auto.
 qed.