intro sch nm h
η : Type u_η
dec_η : DecidableEq η
schema : Schema
⊢ ∀ (sch : Schema) (nm : η), HasName nm sch → nm ∈ map Prod.fst sch
η : Type u_η
dec_η : DecidableEq η
schema : Schema
sch : Schema
nm : η
h : HasName nm sch
⊢ nm ∈ map Prod.fst sch