| | Who Cites hres abstract? |
|
| hres_abstract | Def res_abstract ==  P:'a   . f:'a'b. res_lambda('a;'b;x.P(x);x.f(x)) |
| | | Thm*  'a,'b:S. res_abstract  (('a hbool) ('a 'b) 'a 'b) |
|
| res_lambda | Def res_lambda('a;'b;x.P(x);x.f(x)) == x:'a. if P(x) then f(x) else arb('b) fi |
| | | Thm* 'a,'b:S, P:('a), f:('a'b). res_lambda('a;'b;x.P(x);x.f(x)) 'a'b |
|
| tlambda | Def (x:T. b(x))(x) == b(x) |
|
| arb | Def arb(T) == InjCase(lem(T); x. x, "uu") |
| | | Thm* T:S. arb(T) T |
|
| bif | Def bif(b; bx.x(bx); by.y(by)) == if b x(*) else y(x.x) fi |
| | | Thm* A:Type, b:, x:(bA), y:(( b)A). bif(b; bx.x(bx); by.y(by)) A |
