y == 
(x = y 
T)
T:Type, x,y:T. (x = y) 
q == if p
true else q fip,q:. (p q) 
== {i:
| 0
i } Type SB == 
B<Ai,j:. (ij) Propj == j<ii,j:. (ij) j == if i<j true ; false fii,j:. (i<j) | Some definitions of interest. | |
| bequal | y == (x = y T) |
| T:Type, x,y:T. (x = y) | |
| bor | q == if p true else q fi |
| p,q:. (p q) | |
| label | |
| nat | == {i:| 0i } |
| Type | |
| S | |
| le | B == B<A |
| i,j:. (ij) Prop | |
| le_int | j == j<i |
| i,j:. (ij) | |
| lt_int | j == if i<j true ; false fi |
| i,j:. (i<j) |
About:
 |  |  |  |  |  |  |
 |  |  |  |  |  |  |  |