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