proposition: Theorem ContrIncl : forall S : State, inclState S ((rZPlus zero, rZMinus zero) :: nil).
proof: Proof. intros S; red in |- *; auto with stalmarck. intros i j H'. apply eqStateRzContr with (a := rZPlus zero); auto with datatypes stalmarck. Qed.
imports: Coq(List)