TypeUnary.Nat
data Nat
zero
one
two
three
four
withIsNat
natSucc
natIsNat
natToZ
natEq
natAdd
natMul
class IsNat n
induction
data m :<: n
succLim
data Index lim
unIndex
succI
index0
index1
index2
index3
coerceToIndex