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.