8
12
4399
let x = 2, y = x + 3, z = 2 * y + x + 1 in z ^ 3 * x + y : ℕ
16
let x : ℕ = 5 + 3 in x + x : ℕ