Simplified code structure in Formula.

Since we're using the representation theorem, CNF contains no nested
modal literals anymore and therefore don't need the unique_ptr
workaround to handle circular (and hence incomplete) types.