Why does the kore parser need to know what sort a KItem is, though? If you explicitly type a term or variable, then that explicit type annotation will need to be included. But the sort of the KItem should just be KItem, unless I'm missing something here.