Add the emptyness condition to the boolean evaluation rule in denotation of assertion
Add the emptyness condition to the boolean evaluation rule in denotation of assertion

prg-titech/CertSkel,iasakura/CertSkel