[STATEMENT]
lemma sum_list_map_cons:
  "sum_list (map weight (y # ys)) = weight y + sum_list (map weight ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum_list (map weight (y # ys)) = weight y + sum_list (map weight ys)
[PROOF STEP]
by auto