proposition: Theorem eqConstrStateSimpl : forall (a b : rZ) (S : State), eqConstrState S (rZComp a) b -> eqConstrState S a (rZComp b).
proof: Proof. intros a b S H'; auto with stalmarck. rewrite <- (rZCompInv a); auto with stalmarck. Qed.
imports: Coq(List)