`iIntros.` should always enter proof mode

  Lemma test (s: loc) (x: val) :
    (WP ref InjR x {{ v, WP let: "s'" := v in #() {{ _, True }} }})%I.
  Proof.
    iIntros.
    (* Now I should be in proof mode, but I am not. *)