The (non-)example was added more or less to demonstrate the limitation of our work, but I guess we can still formalize it? @cangiuli @TOTBWF
