逻辑错误还是错误?量词:forall的存在

// Defining a function and giving it a meaning through axiomatization.
function EqualsInt(x: int, y: int) : bool;
axiom (forall x: int, y: int :: EqualsInt(x, y) == (x == y));


procedure main()
{ 
  assert (exists i: int :: i == i);         // Assertion is verified.
  assert (forall i: int :: EqualsInt(i,i)); // Assertion is verified.
  assert (exists i: int :: EqualsInt(i,i)); // Assertion does not hold.
}

为什么前两个断言成立,而最后一个却不成立?