GitLab

This reverts commit daaabf41.  We have tests for
testcase, we shouldn't depend on using arcane features in our definitions for
this purpose.  Also, this exposes that there still is a bug somewhere (see the
FIXME).

This is backwards-compatible; it desugars to a normal application on previous versions

sed -i 's/∀ᵢ/\<obj\>/g; s/∃ᵢ/\<subj\>/g' $(find ./ -name \*.v)

sed -i 's/absolute/objective/g; s/relative/subjective/g; s/Absolute/Objective/g; s/Relative/Subjective/g' $(find ./ -name \*.v)

Based on an earlier MR by @jung.

This change is slightly more invasive than expected: in monPred we were
using the embedding before the BI was defined. With the new setup, this
is no longer possible, because in order to make an instance of the
embedding, we need to know that `monPred` is a BI. As such, we define
`emp`, `⌜ _ ⌝` and friends directly in the model of `monPred` and later
prove that they are equal to a version in terms of the embedding.

As suggested by @jjourdan, and proved in the ordered RA model by @amintimany.

This should solve the paradox in #149.