case nil
α : Type u_1
p✝ : α → Prop
inst✝ : DecidablePred p✝
l : List α
a : α
p : α → Bool
⊢ all [] p = true ↔ ∀ (a : α), a ∈ [] → p a = true

case cons
α : Type u_1
p✝ : α → Prop
inst✝ : DecidablePred p✝
l✝ : List α
a✝ : α
p : α → Bool
a : α
l : List α
ih : all l p = true ↔ ∀ (a : α), a ∈ l → p a = true
⊢ all (a :: l) p = true ↔ ∀ (a_1 : α), a_1 ∈ a :: l → p a_1 = true
α : Type u_1
p✝ : α → Prop
inst✝ : DecidablePred p✝
l : List α
a : α
p : α → Bool
⊢ all l p = true ↔ ∀ (a : α), a ∈ l → p a = true
induction' l with a l ih
no goals
case cons
α : Type u_1
p✝ : α → Prop
inst✝ : DecidablePred p✝
l✝ : List α
a✝ : α
p : α → Bool
a : α
l : List α
ih : all l p = true ↔ ∀ (a : α), a ∈ l → p a = true
⊢ all (a :: l) p = true ↔ ∀ (a_1 : α), a_1 ∈ a :: l → p a_1 = true
simp only [all_cons, Bool.and_coe_iff, ih, forall_mem_cons]
no goals
case nil
α : Type u_1
p✝ : α → Prop
inst✝ : DecidablePred p✝
l : List α
a : α
p : α → Bool
⊢ all [] p = true ↔ ∀ (a : α), a ∈ [] → p a = true
exact iff_of_true rfl (forall_mem_nil _)