Axiom 7 for predicate logic: equality satisfies the euclidean property (which implies symmetry and transitivity, and reflexivity given axiom 6).
axiom ax_7 (a b c: nat): $ a = b -> a = c -> b = c $;