我为达夫尼的σ代数定义了以下datatype，function和lemma。在我看来，引理应该证明，但是我在最后的assert语句中遇到了断言。

datatype Alg = Empty | Complement(a: Alg) | Union(b: Alg,c: Alg)

const S : set<int>

function eval(X: Alg) : set<int>
    decreases X;
{
    match X
    case Empty => {}
    case Complement(a) => S - eval(X.a)
    case Union(b,c) => eval(X.b) + eval(X.c)
}

lemma algebra()
    ensures forall x :: exists y :: eval(y) == S - eval(x);
{
    var l : Alg;
    var c :| c == Complement(l);
    assert eval(c) == S - eval(l);
    assert exists a {:induction false} :: eval(a) == S - eval(l);
    assert forall x :: exists y :: eval(y) == S - eval(x);   // this statement does not prove
}

我的证明遵循以下逻辑：令l为任意Alg（σ-代数），令c为l的补数。因此，对于l，有一个c被评估为S-l的评估。由于l是任意的Alg，因此这不应该推广到所有Alg吗？

请注意，我还尝试按如下方式写出最后一个assert语句，但仍然违反了。

assert forall x {:induction false} :: exists y {:induction false} :: eval(y) == S - eval(x);

有人知道为什么这不能证明我的建议吗？