rfl
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u_η
t : Table sch
cs : ActionList (Schema.removeTypedName τ) sch
c1 c2 : η
this :
  List.map Prod.fst (List.append (Schema.removeTypedNames sch cs) [(c1, η), (c2, τ)]) =
    List.append (List.map Prod.fst (Schema.removeTypedNames sch cs)) (List.map Prod.fst [(c1, η), (c2, τ)])
⊢ List.append (List.map Prod.fst (Schema.removeTypedNames sch cs)) (List.map Prod.fst [(c1, η), (c2, τ)]) =
    List.map Prod.fst (Schema.removeTypedNames sch cs) ++ [c1, c2]
no goals