intro h
case e
α : Type u
β : Type v
γ : Type w
f : α → β → γ
x : Array α
n : Nat
z : Array γ
⊢ ¬n < size x → (if h : n < List.length x.data then z else z) = z
case e
α : Type u
β : Type v
γ : Type w
f : α → β → γ
x : Array α
n : Nat
z : Array γ
h : ¬n < size x
⊢ (if h : n < List.length x.data then z else z) = z