case cons
α : Type u_1
β : Type u_2
inst✝ : BEq α
a : α
b : β
key✝ : α
value✝ : β
tail✝ : AssocList α β
tail_ih✝ :
  toList (replace a b tail✝) = List.replaceF (fun x => bif x.fst == a then some (a, b) else none) (toList tail✝)
⊢ toList
      (match key✝ == a with
      | true => cons a b tail✝
      | false => cons key✝ value✝ (replace a b tail✝)) =
    match bif key✝ == a then some (a, b) else none with
    | none => (key✝, value✝) :: List.replaceF (fun x => bif x.fst == a then some (a, b) else none) (toList tail✝)
    | some a => a :: toList tail✝
α : Type u_1
β : Type u_2
inst✝ : BEq α
a : α
b : β
l : AssocList α β
⊢ toList (replace a b l) = List.replaceF (fun x => bif x.fst == a then some (a, b) else none) (toList l)
induction l <;> simp [replace]
no goals
case cons
α : Type u_1
β : Type u_2
inst✝ : BEq α
a : α
b : β
key✝ : α
value✝ : β
tail✝ : AssocList α β
tail_ih✝ :
  toList (replace a b tail✝) = List.replaceF (fun x => bif x.fst == a then some (a, b) else none) (toList tail✝)
⊢ toList
      (match key✝ == a with
      | true => cons a b tail✝
      | false => cons key✝ value✝ (replace a b tail✝)) =
    match bif key✝ == a then some (a, b) else none with
    | none => (key✝, value✝) :: List.replaceF (fun x => bif x.fst == a then some (a, b) else none) (toList tail✝)
    | some a => a :: toList tail✝
split <;> simp [*]