fact: Fixpoint cont_size (k: cont) : nat := match k with | Kstop => 0%nat | Kseq c k' => (com_size c + cont_size k')%nat | Kwhile b c k' => cont_size k' end.
imports: Coq(Arith ZArith Psatz Bool String List Program.Equality) CDF(Sequences IMP Simulation)