proposition: Lemma denot_ifthenelse: forall b c1 c2 s, denot (IFTHENELSE b c1 c2) s == if beval b s then denot c1 s else denot c2 s.
proof: Proof. unfold denot; intros. rewrite (u_mon (cinterp (IFTHENELSE b c1 c2) s)); cbn. rewrite run_Later. destruct (beval b s); apply eq_later. Qed.
imports: Coq(Arith ZArith Psatz Bool String List) CDF(Sequences IMP)