Why3.thy 124 Bytes