Skip to content
GitLab

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.