| | Some definitions of interest. |
|
| comment | Def Kind of comment: $kind == a |
|
| decidable | Def Dec(P) == P   P |
| | | Thm*  A:Prop. Dec(A)  Prop |
|
| eq_int | Def i= j == if i=j true ; false fi |
| | | Thm* i,j: . (i=j)  |
|
| exists_unique | Def  !x:A. P(x) == x:A. x is the x:A. P(x) |
| | | Thm* A:Type, P:(A  Prop). (!x:A. P(x)) Prop |
|
| fun_over_st | Def x:A st P(x)B(x) == x:{x:A| P(x) }B(x) |
|
| iff | Def P   Q == (P  Q) & (P Q) |
| | | Thm* A,B:Prop. (A B) Prop |
|
| int_seg | Def {i..j } == {k:| i  k < j } |
| | | Thm* m,n:. {m..n} Type |
|
| 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 |
|
| not | Def A == A False |
| | | Thm* A:Prop. (A) Prop |
