intro all
α : Type u_1
xs : List α
p : α → Bool
i : Fin (List.length xs)
⊢ List.all xs p = true → p (List.get xs i) = true
α : Type u_1
xs : List α
p : α → Bool
i : Fin (List.length xs)
all : List.all xs p = true
⊢ p (List.get xs i) = true