match l with
  | []    => simp [build_pairs] at *
  | x::xs => simp [build_pairs] at h in_pairs
             apply Or.elim in_pairs
             intros in_build_pairs
             simp [build_pairs.pairs] at in_build_pairs
             let ⟨y, t⟩ := in_build_pairs
             have left := t.left
             have right := t.right
             simp [Eq.symm right, left]             
             intros in_build_pairs
             simp
             have res := aux xs (build_pairs xs) (by simp) p
             simp [res in_build_pairs]
α : Type u_1
l✝ : List α
pairs✝ : List (α × α)
h✝ : pairs✝ = build_pairs l✝
l : List α
pairs : List (α × α)
h : pairs = build_pairs l
p : α × α
in_pairs : p ∈ build_pairs l
⊢ p.snd ∈ l
no goals