Need inverse of LemmaCardinalityOfSetNoDuplicates

[robin-aws]

This lemma proves this implication:

  lemma LemmaCardinalityOfSetNoDuplicates<T>(s: seq<T>)
    requires HasNoDuplicates(s)
    ensures |ToSet(s)| == |s|

But the opposite implication would also be very useful:

  lemma LemmaNoDuplicatesCardinalityOfSet<T>(s: seq<T>)
    requires |ToSet(s)| == |s|
    ensures HasNoDuplicates(s)

Especially because |ToSet(s)| == |s| is much cheaper to evaluate at runtime than HasNoDuplicates(s) would be (if it was a compiled function method)

[gancherj]

Created pull request. Please let me know if any style fixes are needed :)