Add ghost state and fix definitions for melocoton

This fixes an issue with an ordinals notation (see first commit message) and adds some ghost theories we need.

Both serve the goal of making this branch more compatible with Iris in general (and our project in particular)