[STATEMENT]
lemma reduce_alist_code [code, code_unfold]:
  "reduce (AList_Mapping.Mapping xs) t = reduce_alist xs t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. reduce (AList_Mapping.Mapping xs) t = reduce_alist xs t
[PROOF STEP]
by (induction t arbitrary: xs)
     (auto simp: AList_Mapping_update split: option.split)