proposition: Theorem realizeStateInvAddEq : forall (f : rNat -> bool) (S : State) (i j : rZ), realizeState f (addEq (i, j) S) -> rZEval f i = rZEval f j.
proof: Proof. intros f S i j H'. apply realizeStateInv with (S := addEq (i, j) S); auto with stalmarck. Qed.
imports: Coq(List)