proposition: Lemma Triple_seq: forall P Q R c1 c2, [[P]] c1 [[Q]] -> [[Q]] c2 [[R]] -> [[P]] c1;;c2 [[R]].
proof: Proof. intros; intros s PRE. destruct (H s PRE) as (s1 & EXEC1 & MID). destruct (H0 s1 MID) as (s2 & EXEC2 & POST). exists s2; split. - apply cexec_seq with s1; auto. - exact POST. Qed.
imports: Coq(ZArith Psatz Bool String List Wellfounded Program.Equality) Coq(FunctionalExtensionality) CDF(IMP Sequences)