proposition: Lemma red_determ: forall cs cs1, red cs cs1 -> forall cs2, red cs cs2 -> cs1 = cs2.
proof: Proof. induction 1; intros cs2 R2; inversion R2; subst; eauto. - inversion H3. - inversion H. - assert (EQ: (c2, s2) = (c4, s3)) by auto. congruence. - congruence. - congruence. Qed.
imports: Coq(Arith ZArith Psatz Bool String List Program.Equality) CDF(Sequences Simulation)