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