use 0-cardinality sorts

[c-cube]

call CVC4 with --fmf-empty-sorts to avoid refining recursive functions that are not used. We need to force it to fill other sorts though, by declaring p : sort -> bool, c : sort, and p(c) if we want to ensure that sort is not empty.