Dafny: verify test case of array sorting with duplicates

Given the usual specification of array sorting in Dafny,

method sort(a: array<T>)
  modifies a    
  ensures isSorted(a[..])
  ensures multiset(a[..]) == multiset(old(a[..]))

predicate isSorted(s: seq<T>) {
  forall i, j :: 0 <= i < j < |s| ==> s[i] <= s[j] 
}

Dafny is able to check a "test case" without duplicates (with a small help)

  method testSortWithoutDups() {
    var a := new T[] [9, 4, 6, 3, 8]; 
    assert a[..] == [9, 4, 6, 3, 8]; // small prover helper!
    sort(a);
    assert a[..] == [3, 4, 6, 8, 9];
  }  

But is not able to check a "test case" with duplicates, so I tried using a lemma as follows:

 method testSortWithDups() {
    var a := new T[] [9, 3, 6, 9]; 
    assert a[..] == [9, 3, 6, 9]; // small prover helper!
    sort(a);
    SortingProp(a[..],  [3, 6, 9, 9]);
    assert a[..] ==  [3, 6, 9, 9];
  }

  // State and prove by induction the property that, if two sequences are sorted and have 
  // the same elements, then they must be identical (so sorting has a unique solution). 
  // Most of the proof steps are filled in by Dafny.
  lemma SortingProp(a: seq<T>, b: seq<T>)
    requires isSorted(a) && isSorted(b) && multiset(a) == multiset(b) 
    ensures a == b
  {
    seqProps(a);
    seqProps(b);
    if |a| > 0 {
      SortingProp(a[1..], b[1..]); 
    }
  }

  // Two usefull properties about sequences and their multisets (proved by Dafny alone): 
  lemma seqProps(a: seq<T>) 
    ensures |a| > 0 ==> a == [a[0]] + a[1..] 
    ensures forall i :: 0 <= i < |a| ==> a[i] in multiset(a)
  {}

Is there a better solution?