diff options
Diffstat (limited to 'theories/Zarith/Wf_Z.v')
| -rw-r--r-- | theories/Zarith/Wf_Z.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Zarith/Wf_Z.v b/theories/Zarith/Wf_Z.v index 389db702c..6b015c77f 100644 --- a/theories/Zarith/Wf_Z.v +++ b/theories/Zarith/Wf_Z.v @@ -25,7 +25,7 @@ Require Zsyntax. Then the diagram will be closed and the theorem proved. *) Lemma inject_nat_complete : - (x:Z)`0 <= x` -> (Ex [n:nat](x=(inject_nat n))). + (x:Z)`0 <= x` -> (EX n:nat | x=(inject_nat n)). Destruct x; Intros; [ Exists O; Auto with arith | Specialize (ZL4 p); Intros Hp; Elim Hp; Intros; |