Derive WP lifting and array rules from TWP rules

It's silly that the proofs of the WP lifting and array rules were pretty much exactly the same for TWP and WP.

This MR improves on this situation by deriving the WP rules from the TWP rules. For this, it makes use of the following lemma:

Lemma twp_wp_step s E e P Φ :
  TCEq (to_val e) None →
  ▷ P -∗
  WP e @ s; E [{ v, P ={E}=∗ Φ v }] -∗ WP e @ s; E {{ Φ }}.

Note the premise TCEq (to_val e) None; this way non-valueness can be derived using TC search. I have also ported the WP step lemmas in the same way.