SIMPLE_CHOOSE : term -> thm -> thm
Existentially quantifies a hypothesis of a theorem.
A call SIMPLE_CHOOSE `v` th existentially quantifies a hypothesis of the
theorem over the variable v. It is intended for use when there is only one
hypothesis so that the choice of assumption is unambiguous. In general, it
picks the one that happens to be first in the list.
- FAILURE CONDITIONS
Fails if v is not a variable or if it is free in the conclusion of the
# let th = SYM(ASSUME `x:num = y`);;
val th : thm = x = y |- y = x
# SIMPLE_EXISTS `x:num` th;;
val it : thm = x = y |- ?x. y = x
# SIMPLE_CHOOSE `x:num` it;;
val it : thm = ?x. x = y |- ?x. y = x
The more general function is CHOOSE, but this is simpler in the special case.
- SEE ALSO
CHOOSE, EXISTS, SIMPLE_EXISTS.