Theorem: Array.size_del (GMLInit/Data/Array/Basic.lean)

State before:
α : Type u_1
as : Array α
k : Fin as.size
⊢ (as.del k).size = as.size - 1
Tactic:
simp [del]
State after:
no goals