simp only [Function.comp, Schema.lookup_fst_eq_nm, CertifiedName.val]
case cons.left
η : 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
no goals