cases xs
α : Type u_1
xs : List α
p : α → Bool
all : List.all xs p = true
iv : Nat
ilt : iv < List.length xs
⊢ p (List.get xs { val := iv, isLt := ilt }) = true
case nil
α : Type u_1
p : α → Bool
iv : Nat
all : List.all [] p = true
ilt : iv < List.length []
⊢ p (List.get [] { val := iv, isLt := ilt }) = true

case cons
α : Type u_1
p : α → Bool
iv : Nat
head✝ : α
tail✝ : List α
all : List.all (head✝ :: tail✝) p = true
ilt : iv < List.length (head✝ :: tail✝)
⊢ p (List.get (head✝ :: tail✝) { val := iv, isLt := ilt }) = true