title: When are Dafny sequences equal?
body: <p>Hi  Having defined a function that builds a sequence from a set it is easy to  verify that from equal sets the function must return equal sequences. But this is not what the results look liked</p>
  <pre><code>qr = [3, 1, 2] ==  qt = [1, 2, 3]  ??  
  </code></pre>
  <p>I am using VScode and running what it calls Dafny 0.18.0. There is either a bug in Dafny or a misunderstanding on my part.<br />
  Any corrections welcome.</p>
  <pre><code>predicate setIsSeq&lt;T&gt;(t : set&lt;T&gt;, q : seq&lt;T&gt;) 
  { (|t| == |q|)  ==&gt;
     (forall i :: (0 &lt;= i &lt; |q|) ==&gt; (q[i] in t)) &amp;&amp;
     (forall x :: x in t ==&gt; (x in q))
  }
  function method fSetToSeq&lt;T&gt;(t : set&lt;T&gt;) : (r : seq&lt;T&gt;)
    decreases t 
    ensures setIsSeq(t,r);
   {
    var inner := t; 
    if (|inner| == 0) then [] 
    else (
      var e :| e in inner; 
      var tx := inner - {e};
      var qx := fSetToSeq(tx);
      [e] + qx   )
    }   
    lemma {:induction s1, s2} whatIsSeq&lt;T&gt;(s1 : set&lt;T&gt;, s2 : set&lt;T&gt;)     
    ensures  s1 == s2 ==&gt; fSetToSeq(s1) == fSetToSeq(s2)  {}
  
  method Main() {
  var st:set&lt;nat&gt; := {1,2,3};
  var sr:set&lt;nat&gt; := {3,1,2};
  assert st == sr;
  var qr:seq&lt;nat&gt; := fSetToSeq(sr);
  var qt:seq&lt;nat&gt; := fSetToSeq(st);
  assert qr == qt;
  print &quot;qr = &quot;, qr,&quot; ==  qt = &quot;, qt,&quot;  ??  \n&quot;;
  
  var xr:seq&lt;nat&gt; := [1, 2, 3];
  var yr:seq&lt;nat&gt; := [3, 1, 2];
  print &quot;yr = &quot;, yr,&quot; !=  xr = &quot;, xr,&quot;  ??  \n&quot;;
  assert yr != xr;
  }
  </code></pre>