simp [build_pairs] at *
α : Type u_1
l✝ : List α
pairs✝ : List (α × α)
h✝ : pairs✝ = build_pairs l✝
l : List α
pairs : List (α × α)
p : α × α
h : pairs = build_pairs []
in_pairs : p ∈ build_pairs []
⊢ p.snd ∈ []
no goals