AMBDA-TYPES: some improvements. subst now fully exploited

[helm.git] / matita / contribs / RELATIONAL / NLE / order.ma

diff --git a/matita/contribs/RELATIONAL/NLE/order.ma b/matita/contribs/RELATIONAL/NLE/order.ma
index 71de65d1d3f4e91c580c95b9e3d8ee5378e86235..7ff57caa3e5fec2dd9b8a5ef099a6d70063f0c09 100644 (file)
--- a/matita/contribs/RELATIONAL/NLE/order.ma
+++ b/matita/contribs/RELATIONAL/NLE/order.ma
@@ -38,10 +38,7 @@ theorem nle_irrefl: \forall x. x < x \to False.
 qed.
 
 theorem nle_irrefl_ei: \forall x, z. z <= x \to z = succ x \to False.
- intros 3. elim H; clear H x z;
- [ destruct H1
- | destruct H3. clear H3. subst. auto.
- ].
+ intros 3. elim H; clear H x z; subst. auto.
 qed.
 
 theorem nle_irrefl_smart: \forall x. x < x \to False.