proposition: Theorem eqStateAddEq : forall (S1 S2 : State) (a b : rZ), eqState S1 S2 -> eqState (addEq (a, b) S1) (addEq (a, b) S2).
proof: Proof. intros S1 S2 a b H'; inversion H'; red in |- *; auto with stalmarck. Qed.
imports: Coq(List)