proposition: Lemma denot_assign: forall x a s, denot (ASSIGN x a) s == now (update x (aeval a s) s).
proof: Proof. intros. unroll_delay (denot (ASSIGN x a) s). apply equi_refl. Qed.
imports: Coq(Arith ZArith Psatz Bool String List) CDF(Sequences IMP)