proposition: Lemma denot_while: forall b c s, denot (WHILE b c) s == if beval b s then bind (denot c s) (denot (WHILE b c)) else now s.
proof: Proof. unfold denot; intros. rewrite (u_mon (cinterp (WHILE b c) s)); cbn. destruct (beval b s). - apply run_Bind. - rewrite run_Ret. apply equi_refl. Qed.
imports: Coq(Arith ZArith Psatz Bool String List) CDF(Sequences IMP)