intros h_bound
sz : ℕ
n m : FinInt sz
⊢ toUint n + toUint m < 2 ^ sz → toUint (n + m) = toUint n + toUint m
sz : ℕ
n m : FinInt sz
h_bound : toUint n + toUint m < 2 ^ sz
⊢ toUint (n + m) = toUint n + toUint m