proposition: Theorem reds_to_cexec: forall s c s', star red (c, s) (SKIP, s') -> cexec s c s'.
proof: Proof. intros. dependent induction H. - apply cexec_skip. - destruct b as [c1 s1]. apply red_append_cexec with c1 s1; auto. Qed.
imports: Coq(Arith ZArith Psatz Bool String List Program.Equality) CDF(Sequences Simulation)