proposition: Theorem eqStateInvInv : forall (S : State) (p q : rZ), eqStateRz S (rZComp p) (rZComp q) -> eqStateRz S p q.
proof: Proof. intros S p0 q0 H'; rewrite <- (rZCompInv p0); rewrite <- (rZCompInv q0); auto with stalmarck. Qed.
imports: Coq(List)