Parity (dwa |^ n) = dwa |^ (dwa |-count (dwa |^ n)) by Def1;
hence Parity (2 |^ n) = 2 |^ n ; :: thesis: verum