intros h_scale h_data
τ fixed : List ℕ
scalable : MLIRTy
v₁ v₂ : Vector τ fixed scalable
⊢ v₁.scale = v₂.scale → v₁.data = v₂.data → v₁ = v₂
τ fixed : List ℕ
scalable : MLIRTy
v₁ v₂ : Vector τ fixed scalable
h_scale : v₁.scale = v₂.scale
h_data : v₁.data = v₂.data
⊢ v₁ = v₂