proposition: Remark star_red_seq_step: forall c1 s1 h1 c2 s2 h2, star red (c1, s1, h1) (c2, s2, h2) -> forall c, star red (SEQ c1 c, s1, h1) (SEQ c2 c, s2, h2).
proof: Proof. intros until h2; intros STAR; dependent induction STAR; intros. - apply star_refl. - destruct b as [ [c' s'] h']. eapply star_step; eauto. apply red_seq_step; auto. Qed.
imports: Coq(ZArith Psatz Bool String List Wellfounded Program.Equality) Coq(FunctionalExtensionality PropExtensionality) CDF(IMP Sequences)