如何解决 Dafny 中 let-such-that 表达式中的未确定问题？

问：

下面是一个示例：

function intsetmax(s:set<int>):int
  requires |s| > 0
  ensures  var m := intsetmax(s);
           m in s && forall i :: i in s ==> m >= i
{
  var x :| x in s;
  if |s| == 1 then
    assert |s - {x}| == 0;
    x
  else
    var sy := s - {x};
    var y := intsetmax(sy);
    assert forall i :: i in s ==> i in sy || i == x;
    if x > y then x else y
}

函数“intsetmax”想要在集合中查找 max 元素，但它显示一个错误“要编译，let-such-that 表达式的值必须唯一确定”，因为语句“var x ：|x 在 s 中”。

此代码适用于低于 4.0 的 Dafny 版本，但它报告 4.0 错误。

那么，如何解决呢？我必须将函数设置为“ghost”吗？有什么方法可以获取集合中的元素吗？