proposition: Lemma Triple_ifthenelse: forall P Q b c1 c2, [[atrue b //\\ P]] c1 [[Q]] -> [[afalse b //\\ P]] c2 [[Q]] -> [[P]] IFTHENELSE b c1 c2 [[Q]].
proof: Proof. intros; intros s PRE. destruct (beval b s) eqn:B. - destruct (H s) as (s' & EXEC & POST). split; auto. exists s'; split; auto. constructor; rewrite B; auto. - destruct (H0 s) as (s' & EXEC & POST). split; auto. exists s'; split; auto. constructor; rewrite B; auto. Qed.
imports: Coq(ZArith Psatz Bool String List Wellfounded Program.Equality) Coq(FunctionalExtensionality) CDF(IMP Sequences)