If I write an assertion which vacuously passes(antecedent is never achieved due to some constraints) then is it possible to have a witness for it? I think witness is like a cover for the assertion statement. So, if antecedent never happens then the cover should be uncoverable and there is no witness .
If the assertion is a |-> b and a is never 1 will I get a witness for this assertion?