induction cs with
| nil => simp only [Schema.pick, List.map]
| cons c cs ih =>
  simp only [Schema.pick, List.map, List.cons.injEq]
  apply And.intro
  . simp only [Function.comp, Schema.lookup_fst_eq_nm, CertifiedName.val]
  . exact ih
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
cs : List (CertifiedHeader sch)
⊢ List.map Prod.fst (Schema.fromCHeaders cs) = List.map (Prod.fst ∘ Sigma.fst) cs
no goals