proposition: Lemma red_seq_steps_plus: forall c2 s c s' c', plus red (c, s) (c', s') -> plus red ((c;;c2), s) ((c';;c2), s').
proof: Proof. intros. inversion H; subst. destruct b as [c1 s1]. econstructor. apply red_seq_step; eauto. apply red_seq_steps; auto. Qed.
imports: Coq(Arith ZArith Psatz Bool String List) CDF(Sequences IMP Compil) Coq(Classical Description)