simp [res rr]
case inr
α : Type u_1
l✝ : List α
pairs✝ : List (α × α)
h✝ : pairs✝ = build_pairs l✝
l : List α
pairs : List (α × α)
p : α × α
x : α
xs : List α
h : pairs = List.map (fun x_1 => (x, x_1)) xs ++ build_pairs xs
rr : p ∈ build_pairs xs
res : p ∈ build_pairs xs → p.fst ∈ xs
⊢ p.fst = x ∨ p.fst ∈ xs
no goals