destruct on section variable picks an already-used name

[samuelgruetter]

Axiom Z: Type.
Inductive InstructionSet := RV32I | RV32IM.
Axiom bitwidth: InstructionSet -> Z.

Class bitwidth_iset(width: Z)(iset: InstructionSet): Prop :=
  bitwidth_matches: bitwidth iset = width.

Section FitsStack.
  Context {iset: InstructionSet} {width: Z} {myname: bitwidth_iset width iset}.

  Definition stack_usage_rec: unit. Admitted.

  Goal stack_usage_rec = tt -> False.
    intros. destruct iset.

fails with

Error: myname is already used.

Desired behavior: destruct should succeed, or if that's not possible because of how Section works, a more helpful error message, eg something like cannot destruct iset because it is used implicitly in stack_usage_rec, should be displayed.

Coq version: 8.13.2