have : a = #[] := eq_empty_of_size_eq_zero heq
case h
α : Type u_1
a : Array α
hemp : ¬a.isEmpty = true
heq : a.size = 0
⊢ False
case h
α : Type u_1
a : Array α
hemp : ¬a.isEmpty = true
heq : a.size = 0
this : a = #[]
⊢ False