proposition: Lemma denot_assign: forall x a s, denot (ASSIGN x a) s = Some (update x (aeval a s) s).
proof: Proof. intros. apply denot_some with 1. auto. Qed.
imports: Coq(Arith ZArith Psatz Bool String List) CDF(Sequences IMP Compil) Coq(Classical Description)