isJust package:sbv

isJust :: SymVal a => SMaybe a -> SBool
sbv Data.SBV.Maybe
Check if the symbolic value is not nothing. 
>>> isJust (sNothing :: SMaybe Integer)
False

>>> isJust (sJust (literal "yep"))
True

>>> prove $ \x -> isJust (sJust (x :: SInteger))
Q.E.D.