let a be Nat; :: thesis: Parity (2 * a) = 2 * (Parity a)
Parity (2 * a) = (Parity 2) * (Parity a) by ILP;
hence Parity (2 * a) = 2 * (Parity a) ; :: thesis: verum