fact: Definition measure (impconf: com * cont * store) : nat := match impconf with (c, k, m) => (com_size c + cont_size k)%nat end.
imports: Coq(Arith ZArith Psatz Bool String List Program.Equality) CDF(Sequences IMP Simulation)