power) == if power=
0
1 else base
(basepower-1) fi (recursive)
Thm* 
n,k:
. (nk) 
Thm* n,k:. (nk)
== {i:| 0 < i }
Thm* Type
A == A 
False
Thm* A:Prop. (A) Prop
j == if i=j true ; false fi
Thm* i,j:. i=j 
| exp |
Def (basepower) == if power=0 1 else base(basepower-1) fi (recursive)
Thm*
Thm* |
| nat_plus |
Def == {i:| 0 < i }
Thm* |
| not |
Def A == A False
Thm* |
| eq_int |
Def i=j == if i=j true ; false fi
Thm* |
About:
 |  |  |  |  |  |  |
 |  |  |  |  |  |  |
 |  |  |  |  |