The _iff lemma and contractive instance for is_lock were missing. This MR adds these.
The _iff and _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.