- Unified : some definitions of unified \lambda\delta

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

diff --git a/helm/software/matita/contribs/RELATIONAL/NLE/fwd.ma b/helm/software/matita/contribs/RELATIONAL/NLE/fwd.ma
index dd0a7cea6a958fb9af6de022a7f9a7d5eabedf24..19ad50b9b2aa7c11cae590a0f3ec987ec194e96d 100644 (file)
--- a/helm/software/matita/contribs/RELATIONAL/NLE/fwd.ma
+++ b/helm/software/matita/contribs/RELATIONAL/NLE/fwd.ma
@@ -20,7 +20,7 @@ include "Nat/fwd.ma".
 include "NLE/defs.ma".
 
 theorem nle_gen_succ_1: \forall x,y. x < y \to 
-                         \exists z. y = succ z \land x <= z.
+                        \exists z. y = succ z \land x <= z.
  intros. inversion H; clear H; intros;
  [ apply (eq_gen_succ_zero ? ? H)
  | lapply linear eq_gen_succ_succ to H2 as H0.
@@ -53,7 +53,7 @@ theorem nle_gen_zero_2: \forall x. x <= zero \to x = zero.
 qed.
 
 theorem nle_gen_succ_2: \forall y,x. x <= succ y \to
-                         x = zero \lor \exists z. x = succ z \land z <= y.
+                        x = zero \lor \exists z. x = succ z \land z <= y.
  intros 2; elim x; clear x; intros;
  [ auto
  | lapply linear nle_gen_succ_succ to H1.