Axiom ax_6 | index | src |

Axiom 6 for predicate logic: for any term a (which cannot depend on x), there exists an x which is equal to a.

axiom ax_6 (a: nat) {x: nat}: $ E. x x = a $;