proposition: Theorem eqStateEq : forall (S1 S2 : State) (p q : rZ), eqState S1 S2 -> eqStateRz S1 p q -> eqStateRz S2 p q.
proof: Proof. intros S1 S2 p q H' H'0. apply eqStateIncl with (S1 := S1); auto with stalmarck. inversion H'; auto with stalmarck. Qed.
imports: Coq(List)