- bug fix in destruct

[helm.git] / matita / contribs / RELATIONAL / NPlus / fun.ma

diff --git a/matita/contribs/RELATIONAL/NPlus/fun.ma b/matita/contribs/RELATIONAL/NPlus/fun.ma
index 66847cf934fcc7c603c709bd074a2a481bf8068d..03dd7d0efd17551928787b915277bf7294adf7bc 100644 (file)
--- a/matita/contribs/RELATIONAL/NPlus/fun.ma
+++ b/matita/contribs/RELATIONAL/NPlus/fun.ma
@@ -28,7 +28,7 @@ theorem nplus_mono: \forall p,q,r1. (p + q == r1) \to
  intros 4. elim H; clear H q r1;
  [ lapply linear nplus_inv_zero_2 to H1
  | lapply linear nplus_inv_succ_2 to H3. decompose
- ]; subst; autobatch.
+ ]; destruct; autobatch.
 qed.
 
 theorem nplus_inj_1: \forall p1, q, r. (p1 + q == r) \to