proposition: Lemma eqStateaddEq2 : forall (S : State) (a b p q : rZ), eqStateRz S p q -> eqStateRz (addEq (a, b) S) p q.
proof: Proof. intros S a b p q H'; generalize a b; Elimc H'; clear a b p q S; auto with stalmarck. intros a b S H' a0 b0; apply eqStateRzIn; simpl in |- *; auto with stalmarck. intros a b c S H' H'0 H'1 H'2 a0 b0. apply eqStateRzTrans with (b := b); auto with stalmarck. intros a b c S H' H'0 a0 b0. apply eqStateRzContr with (a := a); auto with stalmarck. Qed.
imports: Coq(List)