Why3.thy 76 Bytes