add singleton_insert_empty

Closed Ralf Jung requested to merge ralf/singleton_insert_empty into master

This is just an unfolding, but with all the typeclasses that is impossible to find out and also not actually useful when applying lemmas.

Merge request reports