| Some definitions of interest. |
|
deq | Def EqDecider(T) == eq:T T    x,y:T. x = y  (eq(x,y)) |
| | Thm* T:Type. EqDecider(T) Type |
|
assert | Def b == if b True else False fi |
| | Thm* b: . b Prop |
|
iff | Def P  Q == (P  Q) & (P  Q) |
| | Thm* A,B:Prop. (A  B) Prop |
|
l_member | Def (x l) == i: . i<||l|| & x = l[i] T |
| | Thm* T:Type, x:T, l:T List. (x l) Prop |