Dafny no tiene ningún problema con esta definición de una función de intersección establecida.

function method intersection(A: set<int>, B: set<int>): (r: set<int>)
{
    set x | x in A && x in B
}

Pero cuando se trata de la unión, Dafny se queja, "una comprensión del conjunto debe producir un conjunto finito, pero la heurística de Dafny no puede descubrir cómo producir un conjunto limitado de valores para 'x'". A y B son finitos, por lo que claramente la unión también lo es.

function method union(A: set<int>, B: set<int>): (r: set<int>)
{
    set x | x in A || x in B
}

¿Qué explica este comportamiento aparentemente discrepante para un principiante?