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).0 voters
The first two options result in the same proof term. The second option is a bit weird because evar is supposed to create a new evar, which is then immediatly unshelved.
In the last option, the new hypthesis will be z := (the_definition : nat) : nat, which is weird due to the redundant type casting.
IMO, the clearest syntax would be unshelve epose (z : nat := _).
I use a plain assert, usually, or unshelve evar if I need it to be transparent.
You can also use simple refine (let x : nat := _ in _). with a similar effect, no ?