[STATEMENT]
lemma case_list_rule:
  "\<lbrakk> l=[] \<Longrightarrow> <P> fn <Q>; \<And>x xs. l=x#xs \<Longrightarrow> <P> fc x xs <Q> \<rbrakk> \<Longrightarrow> 
  <P> case_list fn fc l <Q>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>l = [] \<Longrightarrow> <P> fn <Q>; \<And>x xs. l = x # xs \<Longrightarrow> <P> fc x xs <Q>\<rbrakk> \<Longrightarrow> <P> case l of [] \<Rightarrow> fn | x # xa \<Rightarrow> fc x xa <Q>
[PROOF STEP]
by (auto split: list.split)