`cases` can reorder equally named hypotheses

[digama0]

example (P : Nat → Prop) (a) (h : ∃ n, a = n + 1 ∧ P n) : ∃ n, P n := by
  let ⟨n', e, h⟩ := h
  cases e
  exact ⟨_, h⟩
  -- application type mismatch
  --   Exists.intro ?m.12045 h
  -- argument
  --   h
  -- has type
  --   ∃ n, n' + 1 = n + 1 ∧ P n : Prop
  -- but is expected to have type
  --   P ?m.12045 : Prop

Before the cases, the state is:

P: Nat → Prop
a: Nat
: ∃ n, a = n + 1 ∧ P n
n': Nat
e: a = n' + 1
h: P n'
⊢ ∃ n, P n

The first h: ∃ n, a = n + 1 ∧ P n argument (name elided in the display) is being shadowed by the h: P n' argument. After cases, the state is:

case refl
P: Nat → Prop
n': Nat
: P n'
h: ∃ n, n' + 1 = n + 1 ∧ P n
⊢ ∃ n, P n

Because h: P n' did not need to be rewritten but h: ∃ n, a = n + 1 ∧ P n did, h: ∃ n, a = n + 1 ∧ P n got moved to the end of the hypothesis list, meaning that now h refers to h: ∃ n, a = n + 1 ∧ P n instead of h: P n' and the exact fails.

[sorawee]

I just got hit by this, but from subst rather than cases.