diff options
| -rw-r--r-- | test-suite/success/Omega.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/success/Omega.v b/test-suite/success/Omega.v index 5077dc0bd..0369bfbf9 100644 --- a/test-suite/success/Omega.v +++ b/test-suite/success/Omega.v @@ -54,7 +54,7 @@ Qed. End B. (* From Nicolas Oury (bug #180): handling -> on Set (fixed Oct 2002) *) -Lemma lem7: (A: Set) (i:Z) `i<= 0` -> (`i<= 0` -> A) -> `i<=0`. +Lemma lem4: (A: Set) (i:Z) `i<= 0` -> (`i<= 0` -> A) -> `i<=0`. Intros. Omega. Qed. |