An Efficiently Checkable, Proof-Based Formulation of Vacuity in Model Checking