Map over both sides of a symbolic Either at the same time
>>> let f = uninterpret "f" :: SInteger -> SInteger
>>> let g = uninterpret "g" :: SInteger -> SInteger
>>> prove $ \x -> fromLeft (bimap f g (sLeft x)) .== f x
Q.E.D.
>>> prove $ \x -> fromRight (bimap f g (sRight x)) .== g x
Q.E.D.