case cons
α : Type u_1
β : Type u_2
inst✝ : BEq α
a key✝ : α
value✝ : β
tail✝ : AssocList α β
tail_ih✝ : find? a tail✝ = Option.map (fun x => x.snd) (findEntry? a tail✝)
⊢ (match key✝ == a with
    | true => some value✝
    | false => find? a tail✝) =
    Option.map (fun x => x.snd)
      (match key✝ == a with
      | true => some (key✝, value✝)
      | false => List.find? (fun x => x.fst == a) (toList tail✝))
α : Type u_1
β : Type u_2
inst✝ : BEq α
a : α
l : AssocList α β
⊢ find? a l = Option.map (fun x => x.snd) (findEntry? a l)
induction l <;> simp [find?]
no goals
case cons
α : Type u_1
β : Type u_2
inst✝ : BEq α
a key✝ : α
value✝ : β
tail✝ : AssocList α β
tail_ih✝ : find? a tail✝ = Option.map (fun x => x.snd) (findEntry? a tail✝)
⊢ (match key✝ == a with
    | true => some value✝
    | false => find? a tail✝) =
    Option.map (fun x => x.snd)
      (match key✝ == a with
      | true => some (key✝, value✝)
      | false => List.find? (fun x => x.fst == a) (toList tail✝))
split <;> simp [*]