method Equal?_by_Set(a: int, b: int) returns (result: bool)
  ensures result == (a == b)
{
  // implement without directly comparing a and b, instead put them in a set:
  return true;
}

method Facts_about_Set(s: set<int>, t: set<int>, u: set<int>)
  ensures s + t == t + s                   // '+' is union
  ensures s * t == t * s                   // '*' is intersection
  ensures s * (t + u) == s * t + s * u     // distributivity
  ensures 7 !in s ==> |s + {7}| == |s| + 1 // membership
  ensures s <= s + t + u                   // subset
{
}

method Two_by_Multiset(a: int, b: int) returns (result: int)
  ensures result == 2
{
  var x := multiset{a, b};
  // implement using x:
  return 0;
}