proposition: Lemma red_append_cexec: forall c1 s1 c2 s2, red (c1, s1) (c2, s2) -> forall s', cexec s2 c2 s' -> cexec s1 c1 s'.
proof: Proof. intros until s2; intros STEP. dependent induction STEP; intros. - inversion H; subst. apply cexec_assign. - apply cexec_seq with s2. apply cexec_skip. auto. - inversion H; subst. apply cexec_seq with s'0. eapply IHSTEP; eauto. auto. - apply cexec_ifthenelse. auto. - inversion H0; subst. apply cexec_while_done. auto. - inversion H0; subst. apply cexec_while_loop with s'0; auto. Qed.
imports: Coq(Arith ZArith Psatz Bool String List Program.Equality) CDF(Sequences Simulation)