Axiom
add0
≪
|
index
|
src
|
≫
The base case in the definition of addition.
axiom add0 (a: nat): $ a + 0 = a $;