Axiom
addeq
≪
|
index
|
src
|
≫
Addition respects equalty.
axiom addeq (a b c d: nat): $ a = b -> c = d -> a + c = b + d $;