injectivity of inductive type function

Stream: lean4

[David Hamelin]

Hello,

I am trying to prove the theorem no_idea in the following code:

inductive Vector : Nat → Type u where
| vnil : Vector 0
| vcons : Char → {n : Nat} → Vector n → Vector (n+1)
deriving Repr

theorem this_one_works (h: n₁ = n₂) : Vector n₁ = Vector n₂ :=
by
  rw [h]

theorem no_idea (h: Vector n₁ = Vector n₂) : n₁ = n₂ := sorry

If I had a proof that the type function Vector was injective, it would solve my problem, but I have no idea on how to proceed.

[Johan Commelin]

Btw, I'm not sure this is useful theorem. When would you ever use it?