Skip to content

add singleton_insert_empty

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