proposition: Lemma eqStateContr : forall (S : State) (p q r s : rZ), eqStateRz S p q -> eqStateRz S p (rZComp q) -> eqStateRz S r s.
proof: Proof. intros S p q r s H' H'0. apply eqStateRzContr with (a := q); auto with stalmarck. apply eqStateRzTrans with (b := p); auto with stalmarck. apply eqStateRzSym; auto with stalmarck. Qed.
imports: Coq(List)