proposition: Theorem realizeStateInvComp : forall (f : rNat -> bool) (S : State), realizeState f S -> forall i j : rZ, eqStateRz S i (rZComp j) -> rZEval f i = negb (rZEval f j).
proof: Proof. intros f S H' i j H'0. rewrite <- rZEvalCompInv. apply realizeStateInv with (S := S); auto with stalmarck. Qed.
imports: Coq(List)