fm 2012 problem 2: a0 in indeed a ghost argument
fm 2012 problem 2: a0 in indeed a ghost argument

(we do not have to use the ghost construct here, but it looks nicer)

jpdeplaix/why3,jpdeplaix/why3,ssaavedra/why3,douglas-larocca/why3,douglas-larocca/why3,ssaavedra/why3,douglas-larocca/why3,ssaavedra/why3,jpdeplaix/why3