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