Also add a test case that exercises `unreachable` code generation.
Nat.mod
rfl : 0 % n = 0
decEq
noConfusion