case cons
α : Type u_1
β : Type u_2
p : α → β → Bool
key✝ : α
value✝ : β
tail✝ : AssocList α β
tail_ih✝ :
  toList (eraseP p tail✝) =
    List.eraseP
      (fun x =>
        match x with
        | (a, b) => p a b)
      (toList tail✝)
⊢ toList
      (match p key✝ value✝ with
      | true => tail✝
      | false => cons key✝ value✝ (eraseP p tail✝)) =
    match p key✝ value✝ with
    | true => toList tail✝
    | false => (key✝, value✝) :: List.eraseP (fun x => p x.fst x.snd) (toList tail✝)
α : Type u_1
β : Type u_2
p : α → β → Bool
l : AssocList α β
⊢ toList (eraseP p l) =
    List.eraseP
      (fun x =>
        match x with
        | (a, b) => p a b)
      (toList l)
induction l <;> simp [List.eraseP, cond]
no goals
case cons
α : Type u_1
β : Type u_2
p : α → β → Bool
key✝ : α
value✝ : β
tail✝ : AssocList α β
tail_ih✝ :
  toList (eraseP p tail✝) =
    List.eraseP
      (fun x =>
        match x with
        | (a, b) => p a b)
      (toList tail✝)
⊢ toList
      (match p key✝ value✝ with
      | true => tail✝
      | false => cons key✝ value✝ (eraseP p tail✝)) =
    match p key✝ value✝ with
    | true => toList tail✝
    | false => (key✝, value✝) :: List.eraseP (fun x => p x.fst x.snd) (toList tail✝)
split <;> simp [*]