`iIntros.` fails to introduce `True`
Lemma push_atomic_spec (s: loc) (x: val) :
True -∗ (WP ref InjR x {{ v, WP let: "s'" := v in #() {{ _, True }} }})%I.
Proof.
iIntros "?".
shows an error:
Tactic failure: iIntro: nothing to introduce.