assumption
case intro.zero
α : Type u_1
p : α → Bool
h : α
t : List α
first : p h = true
rest : List.foldr (fun a r => p a && r) true t = true
ilt : Nat.zero < List.length (h :: t)
⊢ p h = true

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