Theorem: List.all_one (MLIR/Util/List.lean)

State before:
α : Type u_1
P : α → Bool
a : α
⊢ all [a] P = true ↔ P a = true
Tactic:
simp [all, foldr]
State after:
no goals