| Some definitions of interest. |
|
assert | Def b == if b True else False fi |
| | Thm* b: . b Prop |
|
choose | Def @x:T. P(x) == InjCase(lem({x:T| P(x) }); x. x, arb(T)) |
| | Thm* T:S, P:(T Type). (@x:T. P(x)) T |
|
iff | Def P  Q == (P  Q) & (P  Q) |
| | Thm* A,B:Prop. (A  B) Prop |
|
rev_implies | Def P  Q == Q  P |
| | Thm* A,B:Prop. (A  B) Prop |
|
stype | Def S == {T:Type| x:T. True } |
| | Thm* S Type{2} |