[STATEMENT]
lemma cwf_cNode_seqOf:
  "cwf (cNode (s, r) cts) \<Longrightarrow> eff r s (fimage seqOf cts)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cwf (cNode (s, r) cts) \<Longrightarrow> eff r s (seqOf |`| cts)
[PROOF STEP]
by (auto elim: cwf.cases)