proposition: Lemma denot_cexec: forall s c s', denot c s = Some s' -> cexec s c s'.
proof: Proof. intros. destruct (denot_charact c s) as (i & LIM). apply cinterp_cexec with i. rewrite LIM by lia. auto. Qed.
imports: Coq(Arith ZArith Psatz Bool String List) CDF(Sequences IMP Compil) Coq(Classical Description)