have : i < as.val.size := by rwa [as.property.1]
n m : Nat
α : Type u_1
as : Vec₂ n m α
i : Nat
hi : i < n
⊢ Array.size as.val[i] = m
n m : Nat
α : Type u_1
as : Vec₂ n m α
i : Nat
hi : i < n
this : i < Array.size as.val
⊢ Array.size as.val[i] = m