case succ iv =>
apply listAllCorrect
assumption
α : Type u_1
p : α → Bool
h : α
t : List α
first : p h = true
rest : List.foldr (fun a r => p a && r) true t = true
iv : Nat
ilt : Nat.succ iv < List.length (h :: t)
⊢ p (List.get t { val := iv, isLt := (_ : Nat.succ iv ≤ List.length t) }) = true
no goals