Alloy: allの意味がわからない

Alloyのallの意味がよくわからない。

enum X {A, B, C}
check {
  all r: X{
    one r
  }
}

これは反例が見つからない。つまり「all r: X {foo}」は「すべての集合Xの 要素 についてfooが成立する」なわけだ。

しかし、このXをX -> Xに置き換えてみると挙動が違う。

enum X {A, B, C}
check {
  all r: X -> X{
    one r
  }
}

これは反例がたくさん見つかる。つまり「all r: X -> X {foo}」は「すべての『XからXへの写像の集合』の部分集合についてfooが成立する」なわけだ。
最初はX -> Xが集合の集合になってるのかと思ったけども、そういうわけでもなく関係(2要素のタプル)の入った集合にすぎない。じゃあ集合の中に関係が入っているのか単なる値が入っているのかによってallの挙動が変わるということ？？

追記

allの対象がスカラーの集合の場合は、数学的なallの記号と同じ挙動を(andの羅列を生成することで)可能なのでそうしてあるが、スカラーでない場合はそれをやると節の数が多すぎになりそうなのでやっていない、ということらしい。