Axiom 6 for predicate logic: for any term a (which cannot depend on x), there exists an x which is equal to a.
a
x
axiom ax_6 (a: nat) {x: nat}: $ E. x x = a $;