iterator - Dafny で有限集合オブジェクトの要素を反復するにはどうすればよいですか?

Question

Dafnyで有限集合オブジェクトの要素を反復処理する最良の方法は何ですか? 動作するコードの例は楽しいでしょう。