1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
|
\DOC EXISTENCE
\TYPE {EXISTENCE : thm -> thm}
\SYNOPSIS
Deduces existence from unique existence.
\KEYWORDS
rule, unique, existential.
\DESCRIBE
When applied to a theorem with a unique-existentially quantified
conclusion, {EXISTENCE} returns the same theorem with normal existential
quantification over the same variable.
{
A |- ?!x. p
------------- EXISTENCE
A |- ?x. p
}
\FAILURE
Fails unless the conclusion of the theorem is unique-existentially quantified.
\EXAMPLE
{
# let th = MESON[] `?!n. n = m`;;
...
val th : thm = |- ?!n. n = m
# EXISTENCE th;;
val it : thm = |- ?n. n = m
}
\SEEALSO
EXISTS, SIMPLE_EXISTS.
\ENDDOC
|
