proposition: Theorem Hoare_sound: forall P c Q, Hoare P c Q -> {{P}} c {{Q}}.
proof: Proof. induction 1; eauto using triple_skip, triple_assign, triple_seq, triple_ifthenelse, triple_while, triple_consequence. Qed.
imports: Coq(ZArith Psatz Bool String List Wellfounded Program.Equality) Coq(FunctionalExtensionality) CDF(IMP Sequences)