'a:S. all(
P:'a 
hbool. all(x:'a. implies(P(x),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. all(P:'a hbool. all(x:'a. implies(P(x),P(select(P))))) | [hselect_ax] |
| 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] |