proposition: Lemma RealizeNegb : forall (S : State) (f : rNat -> bool), realizeState f S -> realizeState (fun n : rNat => negb (f n)) S.
proof: Proof. unfold realizeState in |- *; intros S f Hf i j Hij; generalize (Hf i j Hij); case i; case j; simpl in |- *; intros n m Hnm; rewrite Hnm; auto with stalmarck. Qed.