Take for example wp_pure_step_fupd. The proof state at the very first line looks like this:
...
⊢ Nat.repeat (fun Q => iprop(|={E,E₂}=> ▷ |={E₂,E}=> Q)) n iprop(£ n -∗ WP e₂ @ s ; E {{ Φ }} ) ⊢ WP e₁ @ s ; E {{ Φ }}
ie. a Nat.repeat. Ideally, this would delaborate into the modality in the goal
(|={E}[E₂]▷=>^[n] £ n -∗ WP e₂ @ s; E {{ Φ }}) ⊢ WP e₁ @ s; E {{ Φ }}
Take for example wp_pure_step_fupd. The proof state at the very first line looks like this:
ie. a Nat.repeat. Ideally, this would delaborate into the modality in the goal