Theorem: Fin.any_succ (Extra/Fin.lean)

State before:
n : Nat
p : Fin (n + 1) → Bool
⊢ Fin.any p = (p 0 || Fin.any (p ∘ succ))
Tactic:
simp [Fin.any, Fin.foldr_succ]
State after:
no goals