Theorem: Fin.all_succ (Extra/Fin/Basic.lean)

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