injection error

Stream: lean4

[Nick Chopper]

theorem subtype_inj (A: Type) (p: A → Prop) (a b: A) (pa: p a) (pb: p b) : (⟨a, pa⟩: {a//p a}) = (⟨b, pb⟩: {b//p b}) → a = b := by
  intro eq
  injection eq
  assumption

results in (red line at injection eq)

tactic 'introN' failed, insufficient number of binders
A : Type
p : A → Prop
a b : A
pa : p a
pb : p b
 : a = b
⊢ a = b

[Leonardo de Moura]

Pushed a fix https://github.com/leanprover/lean4/commit/b7a0bdb9c9ba6adade3650c560435031b5cdfa99