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.