Use user-supplied names in iIntros (?)
Similar to !479 (merged), the proof mode should preserve user names in binders in iIntros (?)
.
This depends on !479 (merged) since there's some common infrastructure for representing and threading identifiers through typeclasses.