代入をなくそう

n = 1ではなく

n: 1 (nは1である)
n: Nat (nは自然数である)

これを基礎とする