induction h with
| hd =>
  apply List.Mem.head
| tl _ ih =>
  apply List.Mem.tail
  apply ih
η : Type u_η
dec_η : DecidableEq η
schema : Schema
sch : Schema
nm : η
h : HasName nm sch
⊢ nm ∈ map Prod.fst sch
no goals