If `Maybe a` is `Just a` or `Nothing`, then Erlang's `ok` or `{error, Reason}` should be called `Surely`.
```inductive Maybe (R: Type u) where| just (ok: R)| nothing
inductive Surely (L: Type u) where| ok| error (err: L)```
Mastodon server of https://doma.dev.