| | Who Cites hres select? |
|
| hres_select | Def res_select ==  P:'a   . Q:'a. res_choose('a;x. (P(x));x.(Q(x))) |
| | | Thm*  'a:S. res_select  (('a hbool) ('a hbool) 'a) |
|
| assert | Def b == if b True else False fi |
| | | Thm* b:. b Prop |
|
| res_choose | Def res_choose('a;x.P(x);x.Q(x)) == @x:'a. (P(x) & Q(x)) |
| | | Thm* 'a:S, P,Q:('aProp). res_choose('a;x.P(x);x.Q(x)) 'a |
|
| tlambda | Def (x:T. b(x))(x) == b(x) |
|
| choose | Def @x:T. P(x) == InjCase(lem({x:T| P(x) }); x. x, arb(T)) |
| | | Thm* T:S, P:(TType). (@x:T. P(x)) T |
|
| arb | Def arb(T) == InjCase(lem(T); x. x, "uu") |
| | | Thm* T:S. arb(T) T |
