no goals
α : Type u_1
inst✝ : BEq α
l : List α
a : α
⊢ contains l a = any l fun x => a == x
induction l with simp | cons b l => cases a == b <;> simp [*]
no goals
case cons
α : Type u_1
inst✝ : BEq α
a b : α
l : List α
tail_ih✝ : contains l a = any l fun x => a == x
⊢ (match a == b with
    | true => true
    | false => elem a l) =
    (a == b || any l fun x => a == x)
cases a == b <;> simp [*]