intros p in_pairs
α : Type u_1
l✝ : List α
pairs✝ : List (α × α)
h✝ : pairs✝ = build_pairs l✝
l : List α
pairs : List (α × α)
h : pairs = build_pairs l
⊢ ∀ (p : α × α), p ∈ pairs → p.fst ∈ l
α : 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 ∈ pairs
⊢ p.fst ∈ l