fact: Definition oneState (S : State) (a b : rZ) := match eqStateRzDec S a b with | left _ => 0 | right _ => 1 end.
imports: Stalmarck(state) Coq(Arith) Stalmarck(stateDec) Coq(Inverse_Image) Coq(Compare) Coq(Relation_Definitions)