| Some definitions of interest. |
|
habs_sum | Def abs_sum == f:  'a 'b  . @u:'a+'b. (rep_sum(u) = f   'a 'b  ) |
| | Thm* 'a,'b:S. abs_sum ((hbool  'a  'b  hbool)  hsum('a; 'b)) |
|
hrep_sum | Def rep_sum
Def == u:'a+'b. InjCase(u
Def == u:'a+'b. InjCase; p. b: . x:'a. y:'b. (x = p) b
Def == u:'a+'b. InjCase; q. b: . x:'a. y:'b. (y = q)   b) |
| | Thm* 'a,'b:S. rep_sum (hsum('a; 'b)  hbool  'a  'b  hbool) |
|
band | Def p q == if p q else false fi |
| | Thm* p,q: . (p q)  |
|
bequal | Def x = y ==  (x = y T) |
| | Thm* T:Type, x,y:T. (x = y)  |
|
bnot | Def  b == if b false else true fi |
| | Thm* b: .  b  |
|
hbool | Def hbool ==  |
| | Thm* hbool S |
|
hsum | Def hsum('a; 'b) == 'a+'b |
| | Thm* 'a,'b:S. hsum('a; 'b) S |
|
stype | Def S == {T:Type| x:T. True } |
| | Thm* S Type{2} |
|
tlambda | Def ( x:T. b(x))(x) == b(x) |