| | Some definitions of interest. |
|
| eq_int | Def i= j == if i=j true ; false fi |
| | | Thm*  i,j: . (i=j)   |
|
| sized_bool | Def  a {k} == {p:(a  )| size(a)(p) = k } |
| | | Thm* a,k:. a {k} Type |
|
| sized_mset | Def a {k} T == {p:(aT)| Msize(p) = k } |
| | | Thm* a,k:. a {k} Type |
| | | Thm* a,k,x:, y:. a {k} {x..y } Type |
| | | Thm* a,k,x:, y:. a {k} {x...y} Type |
| | | Thm* a,k:. a {k}  Type |
| | | Thm* a,k,x:. a {k} {x...} Type |
|
| int_seg | Def {i..j} == {k:| i  k < j } |
| | | Thm* m,n:. {m..n} Type |
|
| one_one_corr_2 | Def A ~ B ==  f:(AB), g:(BA). InvFuns(A;B;f;g) |
| | | Thm* A,B:Type. (A ~ B) Prop |
|
| inv_funs_2 | Def InvFuns(A;B;f;g) == (x:A. g(f(x)) = x) & (y:B. f(g(y)) = y) |
| | | Thm* f:(AB), g:(BA). InvFuns(A;B;f;g) Prop |
|
| nat | Def == {i:| 0i } |
| | | Thm* Type |
