[STATEMENT]
lemma sum_case_non [simp]: "\<not> is_sum a \<Longrightarrow> sum_case f g a = undefined"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> is_sum a \<Longrightarrow> sum_case f g a = undefined
[PROOF STEP]
by (simp add: sum_case_def is_sum_def)