simp only [header, Schema.names]
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u_η
t : Table sch
cs : ActionList (Schema.removeTypedName τ) sch
c1 c2 : η
⊢ header (pivotLonger t cs c1 c2) = Schema.names (Schema.removeTypedNames sch cs) ++ [c1, c2]
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u_η
t : Table sch
cs : ActionList (Schema.removeTypedName τ) sch
c1 c2 : η
⊢ List.map Prod.fst (Schema.append (Schema.removeTypedNames sch cs) [(c1, η), (c2, τ)]) =
    List.map Prod.fst (Schema.removeTypedNames sch cs) ++ [c1, c2]