proposition: Lemma triple_seq: forall P Q R c1 c2, {{P}} c1 {{Q}} -> {{Q}} c2 {{R}} -> {{P}} c1;;c2 {{R}}.
proof: Proof. unfold triple; intros. inversion H1; subst. eauto. Qed.
imports: Coq(ZArith Psatz Bool String List Wellfounded Program.Equality) Coq(FunctionalExtensionality) CDF(IMP Sequences)