| Some definitions of interest. |
|
assert | Def b == if b True else False fi |
| | Thm* b: . b Prop |
|
houtl | Def outl == u:'a+'b. InjCase(u; x. x, arb('a)) |
| | Thm* 'a,'b:S. outl (hsum('a; 'b)  'a) |
|
hsum | Def hsum('a; 'b) == 'a+'b |
| | Thm* 'a,'b:S. hsum('a; 'b) S |
|
isl | Def isl(x) == InjCase(x; y. true ; z. false ) |
| | Thm* A,B:Type, x:A+B. isl(x)  |
|
outl | Def outl(x) == InjCase(x; y. y; z. "???") |
| | Thm* A,B:Type, x:A+B. isl(x)  outl(x) A |
|
stype | Def S == {T:Type| x:T. True } |
| | Thm* S Type{2} |