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