. 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
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
no goals