Fin {} = {{}} by Th14, ZFMISC_1:1;