Merged requested to merge robbert/lock_contractive into master
_iff lemma and contractive instance for
is_lock were missing. This MR adds these.
_alter lemmas for invariants had their arguments in inconsistent order. This MR makes them consistent with e.g.,
wp_wand. For example,
inv N P -∗ ▷ □ (P ↔ Q) -∗ inv N Q.