proposition: Lemma Hoare_ifthen: forall b c P Q, Hoare (atrue b //\\ P) c Q -> afalse b //\\ P -->> Q -> Hoare P (IFTHENELSE b c SKIP) Q.
proof: Proof. intros. apply Hoare_ifthenelse; auto. apply Hoare_consequence_pre with Q; auto using Hoare_skip. Qed.
imports: Coq(ZArith Psatz Bool String List Wellfounded Program.Equality) Coq(FunctionalExtensionality) CDF(IMP Sequences)