cases in_pairs
α : Type u_1
l✝ : List α
pairs✝ : List (α × α)
h✝ : pairs✝ = build_pairs l✝
l : List α
pairs : List (α × α)
p : α × α
x : α
xs : List α
h : pairs = build_pairs (x :: xs)
in_pairs : (∃ a, a ∈ xs ∧ (x, a) = p) ∨ p ∈ build_pairs xs
⊢ p.fst ∈ x :: xs
case inl
α : Type u_1
l✝ : List α
pairs✝ : List (α × α)
h✝¹ : pairs✝ = build_pairs l✝
l : List α
pairs : List (α × α)
p : α × α
x : α
xs : List α
h : pairs = build_pairs (x :: xs)
h✝ : ∃ a, a ∈ xs ∧ (x, a) = p
⊢ p.fst ∈ x :: xs

case inr
α : Type u_1
l✝ : List α
pairs✝ : List (α × α)
h✝¹ : pairs✝ = build_pairs l✝
l : List α
pairs : List (α × α)
p : α × α
x : α
xs : List α
h : pairs = build_pairs (x :: xs)
h✝ : p ∈ build_pairs xs
⊢ p.fst ∈ x :: xs