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