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