Use user-supplied names when destructing existentials with ? intro pattern
When running iDestruct "H" as (?) "H", use the name of the binder in
"H". For example, if "H" has type ∃ y, Φ y, we now use y as the
name of the variable after freshening. Previously the name was always
the equivalent of running fresh H.
The implementation achieves this by forwarding the desired identifier
name through the IntoExist typeclass. Identifiers are serialized in
Gallina by using them as the name of a function of type ident_name := unit -> unit.