cases hc
α : Type u
β : Type v
as : Array α
h✝ : size as > 0
l : List α
h : List.length l > 0
hc : l = []
⊢ False
case refl
α : Type u
β : Type v
as : Array α
h✝ : size as > 0
h : List.length [] > 0
⊢ False