Using this new definition we can express being contractive using a
Proper. This has the following advantages:

- It makes it easier to state that a function with multiple arguments
  is contractive (in all or some arguments).
- A solve_contractive tactic can be implemented by extending the
  solve_proper tactic.

This removes Ralf's hack of using later_car, which is not function in the logic.

Thanks to Aleš for suggesting this.

Also, higher cost for [elim_modal_bupd_fupd], so that it is not taken in place of [elim_modal_fupd_fupd] in spec patterns.

No longer `put box_own_prop γ P` in the invariant, it is persistent.

    The idea on magic wand is to use it for curried lemmas and use ⊢ for uncurried lemmas.

Robbert Krebbers authored 8 years ago and Ralf Jung committed 8 years ago

We do this by introducing a type class UpClose with notation ↑.

The reason for this change is as follows: since `nclose : namespace
→ coPset` is declared as a coercion, the notation `nclose N ⊆ E` was
pretty printed as `N ⊆ E`. However, `N ⊆ E` could not be typechecked
because type checking goes from left to right, and as such would look
for an instance `SubsetEq namespace`, which causes the right hand side
to be ill-typed.