Theorem: Cpdt.Chapter3.all_cons (Cpdt/Chapter3/Nested.lean)

State before:
α✝ : Type u_1
p : α✝ → Prop
x : α✝
xs : List α✝
⊢ all p (x :: xs) = (p x ∧ all p xs)
Tactic:
rfl
State after:
no goals