allow specializing a wand with a Coq-level proof of the premise

See merge request FP/iris-coq!154

consistently use iSolveTC to solve typeclass goals

See merge request FP/iris-coq!151

also improve README

Added naming conventions for definitions to naming.txt

See merge request FP/iris-coq!152

This avoids the proofmode to be irritated by unrelated goals with a typeclass
type.

Make uPred itself independent of BI interface and just prove primitive laws (like in master branch)

See merge request FP/iris-coq!148

The BI interface is then instantiated using these laws.  In particular, this
shows that the rules we claim to be admissible actually are.

Fixes #193

Show that atomic_step is an AccElim so we can open invariants; get entirely rid of the Em ⊆ Eo side-condition

New atomic updates: defined as a fixed point with existential quantifier; intro lemma using class of Laterable assertions