[Iris-Club] Two Monoid Questions

[Ralf Jung]

> By defining SProp, I suppose you would also define the logical operators and
> prove that it's an step-indexed intuitionistic logic?

No, I'd just define the notion of down-closed predicates, and show that they
form a COFE.  I'd show that `dist` can be written as one (and maybe validity
too, for fun's sake).  And that's about all I need to get started.

Even independent of a proof mode instance this opens all sorts of questions:
should `dist` be define as one of these? Should `UPred` use this? Should there
be embeddings to/from the Iris Base Logic?
For now, I am only interested in what is needed to generalize auth.

; Ralf