i
j ;x=ji else x fi
k:
, i,j:k. (i, j) 
k
kj == if i=j true ; false fii,j:
. (i=j) 
| Who Cites flip? | |
| flip | Def (i, j)(x) == if x=ij ;x=ji else x fi |
| Thm* k:, i,j:k. (i, j) kk | |
| eq_int | Def i=j == if i=j true ; false fi |
| Thm* i,j:. (i=j) |
| Syntax: | (i, j) | has structure: | flip(i; j) |
About:
 |  |  |  |  |  |
 |  |  |  |  |
 |