simp only [Schema.pick, List.map, List.cons.injEq]
case cons
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
c : CertifiedHeader sch
cs : List (CertifiedHeader sch)
ih : List.map Prod.fst (Schema.fromCHeaders cs) = List.map (Prod.fst ∘ Sigma.fst) cs
⊢ List.map Prod.fst (Schema.fromCHeaders (c :: cs)) = List.map (Prod.fst ∘ Sigma.fst) (c :: cs)
case cons
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
c : CertifiedHeader sch
cs : List (CertifiedHeader sch)
ih : List.map Prod.fst (Schema.fromCHeaders cs) = List.map (Prod.fst ∘ Sigma.fst) cs
⊢ c.fst.fst = (Prod.fst ∘ Sigma.fst) c ∧
    List.map Prod.fst (Schema.map Sigma.fst cs) = List.map (Prod.fst ∘ Sigma.fst) cs