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. *)
