match l with
  | []    => simp [build_pairs] at in_pairs
  | x::xs => simp [build_pairs, build_pairs.pairs] at in_pairs
             cases in_pairs
             rename_i hh
             let ⟨y, t⟩ := hh
             simp
             have right := Eq.symm t.right
             constructor
             simp [right]
             simp [build_pairs, build_pairs.pairs] at h
             simp
             have res := aux xs (build_pairs xs) (by simp) p
             rename_i rr
             simp [res rr]
α : 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.fst ∈ l
no goals