α : Type u_1
β : Type u_2
f : α → β → β
inst✝ : BEq α
a : α
l : AssocList α β
⊢ toList (modify a f l) =
    List.replaceF
      (fun x =>
        match x.fst == a with
        | true => some (a, f x.fst x.snd)
        | false => none)
      (toList l)
α : Type u_1
β : Type u_2
f : α → β → β
inst✝ : BEq α
a : α
l : AssocList α β
⊢ toList (modify a f l) =
    List.replaceF
      (fun x =>
        match x with
        | (k, v) => bif k == a then some (a, f k v) else none)
      (toList l)
simp [cond]
no goals
α : Type u_1
β : Type u_2
f : α → β → β
inst✝ : BEq α
a : α
l : AssocList α β
⊢ toList (modify a f l) =
    List.replaceF
      (fun x =>
        match x.fst == a with
        | true => some (a, f x.fst x.snd)
        | false => none)
      (toList l)
induction l with simp [List.replaceF]
| cons k v es ih => cases k == a <;> simp [ih]
no goals
case cons
α : Type u_1
β : Type u_2
f : α → β → β
inst✝ : BEq α
a k : α
v : β
es : AssocList α β
ih :
  toList (modify a f es) =
    List.replaceF
      (fun x =>
        match x.fst == a with
        | true => some (a, f x.fst x.snd)
        | false => none)
      (toList es)
⊢ toList
      (match k == a with
      | true => cons a (f k v) es
      | false => cons k v (modify a f es)) =
    match
      match k == a with
      | true => some (a, f k v)
      | false => none with
    | none =>
      (k, v) ::
        List.replaceF
          (fun x =>
            match x.fst == a with
            | true => some (a, f x.fst x.snd)
            | false => none)
          (toList es)
    | some a => a :: toList es
cases k == a <;> simp [ih]