simp [find?]
case swap
α : Type u_1
a b : List α
f : α → Bool
hunique : ∀ (a1 a2 : α), f a1 = true → f a2 = true → a1 = a2
x✝ y✝ : α
l✝ : List α
⊢ find? f (y✝ :: x✝ :: l✝) = find? f (x✝ :: y✝ :: l✝)
case swap
α : Type u_1
a b : List α
f : α → Bool
hunique : ∀ (a1 a2 : α), f a1 = true → f a2 = true → a1 = a2
x✝ y✝ : α
l✝ : List α
⊢ (match f y✝ with
    | true => some y✝
    | false =>
      match f x✝ with
      | true => some x✝
      | false => find? f l✝) =
    match f x✝ with
    | true => some x✝
    | false =>
      match f y✝ with
      | true => some y✝
      | false => find? f l✝