In some proofs it might be necessary to define some constant using the proof mode. Which of the following variants would you prefer / find more elegant?

`unshelve evar (y : nat).`

`unshelve refine (let x : nat := _ in _).`

`unshelve epose (z := _ : nat).`

- Other?

0 voters