Add lemma `inv_combine`.

This lemma came up in a discussion with @simonspies @jtassaro @lgaeher and @dreyer.

it allows to turn two invariants into one. It's something nice we can do with semantic invariants, but not with the old invariants.