- new tactic subst removes simple non recursive equalities from the context

[helm.git] / helm / software / matita / contribs / RELATIONAL / NLE / dec.ma

diff --git a/helm/software/matita/contribs/RELATIONAL/NLE/dec.ma b/helm/software/matita/contribs/RELATIONAL/NLE/dec.ma
index 6bdb81946269bb7313a9d95f0ab2197962ddd4bb..436dc7e62788ed5df336ef849fc223889a037e33 100644 (file)
--- a/helm/software/matita/contribs/RELATIONAL/NLE/dec.ma
+++ b/helm/software/matita/contribs/RELATIONAL/NLE/dec.ma
@@ -21,11 +21,9 @@ theorem nat_dec_lt_ge: \forall x,y. x < y \lor y <= x.
  [ auto
  | decompose;
    [ lapply linear nle_gen_succ_1 to H1. decompose.
-     rewrite > H1. clear H1 n. auto
+     subst. auto
    | lapply linear nle_lt_or_eq to H1; decompose;
-     [ auto
-     | rewrite > H. clear H n. auto
-     ]
+     subst; auto
    ]
  ].
 qed.