[STATEMENT]
lemma D_None[iff]: "\<D> (e::'a exp) None" and [iff]: "\<D>s (es::'a exp list) None"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D> e None &&& \<D>s es None
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D> e None &&& \<D>s es None
[PROOF STEP]
by(induct e and es rule: \<D>.induct \<D>s.induct)(simp_all)