In reply to dave_59:
This isn’t strictly true. Another example of vacuity is given in section 16.12.16 of the 2012 LRM, where a case property without a matching case item and no default passes vacuously. You can say that such a case is the same as unrolling each case item into an own implication property.
Implication is what “generates” vacuity, but it’s not just possible if you explicitly see an implication property (i.e. ‘|->’ or ‘|=>’ as described in 16.12.6), but also for other properties that have “implication” built into them.