Why3.thy 129 Bytes