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

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

diff --git a/helm/software/matita/contribs/RELATIONAL/NLE/props.ma b/helm/software/matita/contribs/RELATIONAL/NLE/props.ma
index e961f5a9ced40c39a053ab7d7d07f88455a91bc8..8745e160e4b94c6ae1e5e4d6565839a38f634732 100644 (file)
--- a/helm/software/matita/contribs/RELATIONAL/NLE/props.ma
+++ b/helm/software/matita/contribs/RELATIONAL/NLE/props.ma
@@ -28,11 +28,9 @@ theorem nle_lt_or_eq: \forall y,x. x <= y \to x < y \lor x = y.
  intros 1. elim y; clear y; intros;
  [ lapply linear nle_gen_zero_2 to H. auto
  | lapply linear nle_gen_succ_2 to H1. decompose;
-   [ rewrite > H1. clear H1. auto
+   [ subst. auto
    | lapply linear H to H3 as H0. decompose;
-     [ rewrite > H1. clear H1 x. auto
-     | rewrite < H. clear H n. auto
-     ]
+     subst; auto
    ]
  ].
 qed.