cases tactic failed, unexpected failure when introducing aux

Stream: new members

[Horatiu Cheval]

In the following, var is a constructor depending on a natural index and a proof of a statement about it. I believe I am not mistaken in thinking that var i hi = var j hj -> i = j, as I am trying to show below. However, my go-to approach of using cases on var i hi = var j hj fails.
What's happening here? Any ideas on how to solve this?

import tactic

inductive type
| zero : type
| arrow : type → type → type

def context := list type

inductive term : context → type → Type
| var {ctx : context} {σ : type} (i : ℕ) : ctx.nth i = some σ → term ctx σ

open term

example {ctx : context} {σ : type} {i j : ℕ} {hi} {hj} :
  @var ctx σ i hi = @var ctx σ j hj → i = j :=
begin
  intros h,
  cases h,
    /-
  cases tactic failed, unexpected failure when introducing auxiliary equalities
  state:
  ctx : context,
  σ : type,
  i : ℕ,
  hi hj : list.nth ctx i = some σ,
  h : var i hi = var i hj
  ⊢ i = i
  -/
end

[Kevin Buzzard]

example {ctx : context} {σ : type} {i j : ℕ} {hi} {hj} :
  @var ctx σ i hi = @var ctx σ j hj → i = j :=
begin
  intros h,
  injection h,
end

[Horatiu Cheval]

Thanks, I didn't know about injection

[Kevin Buzzard]

Shing Tak Lam told me about it last week :-)

[Eric Wieser]

A shorter proof:

example {ctx : context} {σ : type} {i j : ℕ} {hi} {hj} :
  @var ctx σ i hi = @var ctx σ j hj → i = j :=
var.inj