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. unfold triple, aand, atrue, afalse; intros. inversion H1; subst. destruct (beval b s) eqn:B; eauto. Qed.
imports: Coq(ZArith Psatz Bool String List Wellfounded Program.Equality) Coq(FunctionalExtensionality) CDF(IMP Sequences)