Theorem: Vec₂.size_val (Aoc2023/Utils.lean)

State before:
n m : Nat
α : Type u_1
as : Vec₂ n m α
⊢ Array.size as.val = n
Tactic:
rw [as.property.1]
State after:
no goals