proposition: Lemma cexec_denot: forall s c s', cexec s c s' -> denot c s = Some s'.
proof: Proof. induction 1; intros. - apply denot_skip. - apply denot_assign. - rewrite denot_seq, IHcexec1; auto. - rewrite denot_ifthenelse. destruct (beval b s); auto. - rewrite denot_while, H. auto. - rewrite denot_while, H, IHcexec1; auto. Qed.
imports: Coq(Arith ZArith Psatz Bool String List) CDF(Sequences IMP Compil) Coq(Classical Description)