ac_rfl
case cons
α : Type
inst✝ : BEq α
x : α
bs : List α
a : α
as' : List α
ih : List.count x (as' ++ bs) = List.count x as' + List.count x bs
⊢ (bif a == x then 1 else 0) + (List.count x as' + List.count x bs) =
    (bif a == x then 1 else 0) + List.count x as' + List.count x bs
no goals