removed ll07: very similar to Set.image_Un from the library
removed RelationProperties.inverse and anything that depends on it, as Relation.converse had existed in the library
… but, and that's a cool contribution of ours, without suitable code equations, so I added one!
Theorems are easy to prove with Relation.converse
(Note: the missing code equation probably was the reason why I thought we'd have to define our own "inverse" in the first place, but now I've understood how to create code equations; see "isabelle doc codegen" section 2.2.)