Specware has a base library that is implicitly imported by every spec. Unfortunately, the axioms in this library are not necessarily written to be useful by Snark. Instead of having Snark use these libraries we have created a separate base library for Snark. This library is located at /Library/Base/ProverBase.sw. The axioms in this spec are automatically sent to Snark as part of any proof.