case mk iv ilt => 
cases xs
. contradiction
. case cons h t =>
  simp [List.all, List.foldr] at all 
  cases all with | intro first rest =>
  cases iv <;> simp [List.get]
  assumption
  case succ iv =>
  apply listAllCorrect
  assumption
α : 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
no goals