induction h with
| nil => simp
| cons => simp [find?]; split <;> simp [*]
| swap =>
  simp [find?]; split <;> split <;> simp
  apply hunique; repeat assumption
| trans =>
  simp_all
α : Type u_1
a b : List α
f : α → Bool
hunique : ∀ (a1 a2 : α), f a1 = true → f a2 = true → a1 = a2
h : a ~ b
⊢ find? f a = find? f b
no goals