proposition: Lemma realizeStateEvalAux2 : forall (f : rNat -> bool) (p q r s : rZ) (S : State) (EqS : eqStateRz S p q), (rZEval f p = rZEval f q -> rZEval f r = rZEval f s) -> realizeState f S -> realizeState f (addEq (r, s) S).
proof: Proof. intros f p q r s S H' H'0 H'1. lapply H'0; [ intros H'2 | idtac ]. apply realizeStateAddEq; auto with stalmarck. apply realizeStateInv with (S := S); auto with stalmarck. Qed.