theorem alnex {x: nat} (a: wff x): $ A. x ~a <-> ~E. x a $;
A. x ~a <-> ~~A. x ~a
A. x ~a <-> ~E. x a