'a:S. equal(exists,
P:'a 
hbool. P(select(P)))'a:S, P,Q:('aProp).
Thm* (
x:'a. Q(x) 
P(x)) (
x:'a. Q(x)) P(@x:'a. Q(x))| Theorem | Name |
| 'a:S. equal(exists,P:'a hbool. P(select(P))) | [hexists_def] |
| cites the following: | |
| 'a:S, P,Q:('aProp).
Thm* ( x:'a. Q(x) P(x)) (x:'a. Q(x)) P(@x:'a. Q(x)) | [choose_elim_pos] |