let a be Integer; :: thesis: parity (Parity a) = parity a

per cases ( a is even or a is odd ) ;

suppose A1: a is even ; :: thesis: parity (Parity a) = parity a

then Parity a is even ;
hence parity (Parity a) = parity a by A1; :: thesis: verum

end;

suppose A1: a is odd ; :: thesis: parity (Parity a) = parity a

then Parity a is odd ;
hence parity (Parity a) = parity a by A1; :: thesis: verum

end;

end;