A previous blog explored the verification of the formal hashed sets package in SPARKlib. This post will explain the techniques used to simplify the proof by hiding unnecessary information from the solvers.