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. intros. set (c := if beval b s then c1 else c2). destruct (denot_charact c s) as (i & LIM). apply denot_unique with (S i). intros. destruct j as [ | j]. lia. cbn. rewrite LIM by lia. unfold c; destruct (beval b s); auto. Qed.
imports: Coq(Arith ZArith Psatz Bool String List) CDF(Sequences IMP Compil) Coq(Classical Description)