Should I be bothered that "=" is (((x•x)•(y•y))•(x•y)) so if he's going to write his axiom in terms of NAND, he needs to write all of it using NAND?