second package:sbv

Map over the right side of an Either

>>> let f = uninterpret "f" :: SInteger -> SInteger

>>> prove $ \x -> second f (sRight x :: SEither Integer Integer) .== sRight (f x)
Q.E.D.

>>> prove $ \x -> second f (sLeft x :: SEither Integer Integer) .== sLeft x
Q.E.D.

In the second query we create a new variable z, and then a symbolic query using information from the first query and return a solution that uses the new variable and the old variables. Each child query is run in a separate instance of z3 so you can think of this query as driving to a point in the search space, then waiting for more information, once it gets that information it will run a completely separate computation from the first one and return its results.