Theorem: List.fst_mem_of_pair_mem (Table/BuiltinExtensions.lean)

State before:
α : Type u_1
β : Type u_2
x : α
y : β
hxy : (x, y) ∈ []
⊢ x ∈ map Prod.fst []
Tactic:
contradiction
State after:
no goals