bimap f g empty == empty bimap f g . vertex == vertex . Data.Bifunctor.bimap f g bimap f g (edge x y) == edge (f x) (g y) bimap id id == id bimap f1 g1 . bimap f2 g2 == bimap (f1 . f2) (g1 . g2)
>>> 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.