diff --git a/.github/workflows/ci.yaml b/.github/workflows/ci.yaml
index e4d3ad1..23f34d4 100644
--- a/.github/workflows/ci.yaml
+++ b/.github/workflows/ci.yaml
@@ -20,8 +20,8 @@ jobs:
       - uses: actions/checkout@v3
       - name: install danfy
         run: |
-          wget -q https://github.com/dafny-lang/dafny/releases/download/v3.6.0/dafny-3.6.0-x64-ubuntu-16.04.zip
-          unzip -qq dafny-3.6.0-x64-ubuntu-16.04.zip
+          wget -q https://github.com/dafny-lang/dafny/releases/download/v4.1.0/dafny-4.1.0-x64-ubuntu-20.04.zip
+          unzip -qq dafny-4.1.0-x64-ubuntu-20.04.zip
           echo "dafny=$PWD/dafny/dafny" >> $GITHUB_ENV
       - name: test
         env:
diff --git a/count.dfy b/count.dfy
index 7f4f0a6..e41c3bf 100644
--- a/count.dfy
+++ b/count.dfy
@@ -1,4 +1,4 @@
-function count_eq<T>(x: T, s: seq<T>): nat
+function count_eq<T(==)>(x: T, s: seq<T>): nat
 {
   if s == [] then
     0
@@ -24,27 +24,27 @@ lemma count_multiset<T>(x: T, s: seq<T>)
 {
   if s == [] {
   }
-/*  
-  else if x == s[0] {
-    calc {
-      count_eq(x, s);
-      1 + count_eq(x, s[1..]);
-      multiset{s[0]}[x] + count_eq(x, s[1..]);
-      multiset{s[0]}[x] + multiset(s[1..])[x];
-      multiset([s[0]] + s[1..])[x];
-      { assert s == [s[0]] + s[1..]; }
-      multiset(s)[x];
-    }
-  } 
-*/
+  /*  
+    else if x == s[0] {
+      calc {
+        count_eq(x, s);
+        1 + count_eq(x, s[1..]);
+        multiset{s[0]}[x] + count_eq(x, s[1..]);
+        multiset{s[0]}[x] + multiset(s[1..])[x];
+        multiset([s[0]] + s[1..])[x];
+        { assert s == [s[0]] + s[1..]; }
+        multiset(s)[x];
+      }
+    } 
+  */
   else {
     assert s == [s[0]] + s[1..];
-//    calc {
-//      count_eq(x, s);
-//      (if x == s[0] then 1 else 0) + count_eq(x, s[1..]);
-//      multiset{s[0]}[x] + multiset(s[1..])[x];
-//      { assert s == [s[0]] + s[1..]; }
-//      multiset(s)[x];
-//    }
+    //    calc {
+    //      count_eq(x, s);
+    //      (if x == s[0] then 1 else 0) + count_eq(x, s[1..]);
+    //      multiset{s[0]}[x] + multiset(s[1..])[x];
+    //      { assert s == [s[0]] + s[1..]; }
+    //      multiset(s)[x];
+    //    }
   }
 }
diff --git a/getAllShuffledDataEntriesWithAvoidSet.dfy b/getAllShuffledDataEntriesWithAvoidSet.dfy
index 54e8f3a..92ecf90 100644
--- a/getAllShuffledDataEntriesWithAvoidSet.dfy
+++ b/getAllShuffledDataEntriesWithAvoidSet.dfy
@@ -15,7 +15,7 @@ method swap<T>(a: array<T>, i: int, j: int)
   a[j] := t;
 }
 
-predicate uniq<T>(s: seq<T>)
+predicate uniq<T(==)>(s: seq<T>)
 {
   forall x :: x in s ==> multiset(s)[x] == 1
 }
@@ -117,26 +117,26 @@ method getAllShuffledDataEntriesWithAvoidSet<T(==, 0)>(m_workList: array<T>, avo
   }
 
   if n > 0 {
-//    assert j == k + 1;
-//    assert forall i :: k < i < result.Length ==> result[i] in avoidSet;
-//    assert forall i :: 0 <= i <= k ==> result[i] !in avoidSet;
+    //    assert j == k + 1;
+    //    assert forall i :: k < i < result.Length ==> result[i] in avoidSet;
+    //    assert forall i :: 0 <= i <= k ==> result[i] !in avoidSet;
 
     calc {
-      2 * |avoidSet| - k - 1;
-      <= m_workList.Length - k - 1;
-      == |multiset(result[k+1..])|;
-      <= { suffix_multiset_subset(result[..], k + 1);
-          card_multiset_subset(multiset(result[k+1..]), multiset(avoidSet)); }
-      |avoidSet|;
+       2 * |avoidSet| - k - 1;
+    <= m_workList.Length - k - 1;
+    == |multiset(result[k+1..])|;
+    <= { suffix_multiset_subset(result[..], k + 1);
+         card_multiset_subset(multiset(result[k+1..]), multiset(avoidSet)); }
+       |avoidSet|;
     }
 
-//    assert |avoidSet| <= j; // a contradiction with j + n == |avoidSet| && n > 0
+    //    assert |avoidSet| <= j; // a contradiction with j + n == |avoidSet| && n > 0
   } else {
     // assume multiset(result[..]) == multiset(m_workList[..]);
-  // assume result.Length == m_workList.Length;
-  assert uniq(m_workList[..]);
-  // assume uniq(result[..]);
-  // assume forall i :: 0 <= i < |avoidSet| ==> result[i] !in avoidSet;
+    // assume result.Length == m_workList.Length;
+    assert uniq(m_workList[..]);
+    // assume uniq(result[..]);
+    // assume forall i :: 0 <= i < |avoidSet| ==> result[i] !in avoidSet;
 
   }
 }
diff --git a/getRandomDataEntry.dfy b/getRandomDataEntry.dfy
index 67f52f7..ccafc1d 100644
--- a/getRandomDataEntry.dfy
+++ b/getRandomDataEntry.dfy
@@ -15,7 +15,7 @@ method swap<T>(a: array<T>, i: int, j: int)
   a[j] := t;
 }
 
-predicate uniq<T>(s: seq<T>)
+predicate uniq<T(==)>(s: seq<T>)
 {
   forall x :: x in s ==> multiset(s)[x] == 1
 }
@@ -26,10 +26,10 @@ lemma uniq_multiset_subset<T>(s1: seq<T>, s2: seq<T>)
   ensures multiset(s1) <= multiset(s2)
 {
   forall x | x in s1 ensures multiset(s1)[x] <= multiset(s2)[x] {
-//    calc {
-//      1;
-//      multiset(s1)[x];
-//    }
+    //    calc {
+    //      1;
+    //      multiset(s1)[x];
+    //    }
   }
 }
 
@@ -41,10 +41,10 @@ lemma card_multiset_subset<T>(m1: multiset<T>, m2: multiset<T>)
   }
   else {
     var x :| x in m1;
-//    assert x in m2;
-//    assert |m1| == |m1 - multiset{x}| + 1;
-//    assert |m2| == |m2 - multiset{x}| + 1;
-//    assert m1 - multiset{x} <= m2 - multiset{x};
+    //    assert x in m2;
+    //    assert |m1| == |m1 - multiset{x}| + 1;
+    //    assert |m2| == |m2 - multiset{x}| + 1;
+    //    assert m1 - multiset{x} <= m2 - multiset{x};
     card_multiset_subset(m1 - multiset{x}, m2 - multiset{x});
   }
 }
@@ -84,21 +84,21 @@ method getRandomDataEntry<T(==)>(m_workList: array<T>, avoidSet: seq<T>) returns
   }
 
   calc {
-       m_workList.Length;
-    == |multiset(m_workList[..])|;
-    <= { uniq_multiset_subset(m_workList[..], avoidSet);
-        card_multiset_subset(multiset(m_workList[..]), multiset(avoidSet)); }
-       |multiset(avoidSet)|;
-    == |avoidSet|; // a contradiction!
+     m_workList.Length;
+  == |multiset(m_workList[..])|;
+  <= { uniq_multiset_subset(m_workList[..], avoidSet);
+       card_multiset_subset(multiset(m_workList[..]), multiset(avoidSet)); }
+     |multiset(avoidSet)|;
+  == |avoidSet|; // a contradiction!
   }
-//  assert forall x :: x in m_workList[..] ==> x in avoidSet;
-//  assert uniq(m_workList[..]);
-//  multiset_subset(m_workList[..], avoidSet);
-//  assert multiset(m_workList[..]) <= multiset(avoidSet);
-//  card_multiset_subset(multiset(m_workList[..]), multiset(avoidSet));
-//  assert |multiset(m_workList[..])| <= |multiset(avoidSet)|;
-//  assert false;
-  
+  //  assert forall x :: x in m_workList[..] ==> x in avoidSet;
+  //  assert uniq(m_workList[..]);
+  //  multiset_subset(m_workList[..], avoidSet);
+  //  assert multiset(m_workList[..]) <= multiset(avoidSet);
+  //  card_multiset_subset(multiset(m_workList[..]), multiset(avoidSet));
+  //  assert |multiset(m_workList[..])| <= |multiset(avoidSet)|;
+  //  assert false;
+
   return m_workList[0];
 }
 
@@ -118,7 +118,7 @@ method fillWithRandomDataEntries<T(==, 0)>(m_workList: array<T>, n: int, avoidSe
 
   var k := m_workList.Length - 1;
   var r := 0;
-  
+
   while (k >= 0 && r < n)
     invariant k >= -1
     invariant r <= n
@@ -142,42 +142,42 @@ method fillWithRandomDataEntries<T(==, 0)>(m_workList: array<T>, n: int, avoidSe
       assert forall x :: x in out[0..r] ==> x in m_workList[(k + 1)..] && x !in avoidSet;
       // assert multiset(out[0..r]) <= multiset(m_workList[..]);
 
-//      assert e == m_workList[k];
+      //      assert e == m_workList[k];
       suffix_multiset_subset(m_workList[..], k);
       assert multiset(m_workList[k..]) <= multiset(m_workList[..]);
-//      assert uniq(m_workList[k..]);
+      //      assert uniq(m_workList[k..]);
 
       if e in out[0..r] {
         assert e in m_workList[(k + 1)..];
         calc {
-          multiset(m_workList[k..])[e];
+           multiset(m_workList[k..])[e];
           { assert m_workList[k..] == m_workList[k..k+1] + m_workList[k+1..]; }
-          multiset(m_workList[k..k+1] + m_workList[k+1..])[e];
-          >= 2; // a contradiction!
+           multiset(m_workList[k..k+1] + m_workList[k+1..])[e];
+        >= 2; // a contradiction!
         }
       }
-//      assert e !in out[0..r];
-      
+      //      assert e !in out[0..r];
+
       r := r + 1;
     }
-    
+
     k := k - 1;
   }
 
   if r < n {
-//    assert k == -1;
-//    assert forall x :: x in m_workList[..] ==> x in avoidSet || x in out[0..r];
-//    assert forall x :: x in m_workList[..] ==> x in avoidSet + out[0..r];
+    assert k == -1;
+    assert forall x :: x in m_workList[..] ==> x in avoidSet || x in out[0..r];
+    assert forall x :: x in m_workList[..] ==> x in avoidSet + out[0..r];
 
     uniq_multiset_subset(m_workList[..], avoidSet + out[0..r]);
     card_multiset_subset(multiset(m_workList[..]), multiset(avoidSet + out[0..r]));
 
-//    assert false;
+    //    assert false;
   }
   else {
-//    assert r == n;
+    //    assert r == n;
     assert out[0..n] == out[..];
   }
 
-//  assert r == n;
+  //  assert r == n;
 }
diff --git a/leetcode/0026-remove-duplicates-sorted.dfy b/leetcode/0026-remove-duplicates-sorted.dfy
index 90d8b85..c9a655b 100644
--- a/leetcode/0026-remove-duplicates-sorted.dfy
+++ b/leetcode/0026-remove-duplicates-sorted.dfy
@@ -19,6 +19,7 @@ method RemveDuplicates(nums: array<int>) returns (length: int)
     invariant SortedStrict(nums[..j + 1])
     invariant i < nums.Length ==> forall k :: 0 <= k < i ==> nums[k] <= nums[i]
     invariant forall k :: 0 <= k < i ==> old(nums[k]) in nums[..j + 1]
+    invariant i < nums.Length ==> nums[j] <= nums[i]
   {
     if nums[i] != nums[j] {
       j := j + 1;
diff --git a/leetcode/0027-remove-element.dfy b/leetcode/0027-remove-element.dfy
index 0f60fcb..a507851 100644
--- a/leetcode/0027-remove-element.dfy
+++ b/leetcode/0027-remove-element.dfy
@@ -1,23 +1,24 @@
 method RemoveElement(nums: array<int>, val: int) returns (newLength: int)
-    modifies nums
-    ensures 0 <= newLength <= nums.Length
-    ensures forall x :: x in nums[..newLength] ==> x != val
-    ensures multiset(nums[..newLength]) == multiset(old(nums[..]))[val := 0]
+  modifies nums
+  ensures 0 <= newLength <= nums.Length
+  ensures forall x :: x in nums[..newLength] ==> x != val
+  ensures multiset(nums[..newLength]) == multiset(old(nums[..]))[val := 0]
 {
-    var i := 0;
-    var j := 0;
-    while i < nums.Length
-        invariant j <= i
-        invariant i <= nums.Length
-        invariant old(nums[i..]) == nums[i..];
-        invariant multiset(nums[..j]) == multiset(old(nums[..i]))[val := 0]
-    {
-        if nums[i] != val {
-            nums[j] := nums[i];
-            j := j + 1;
-        }
-        i := i + 1;
+  var i := 0;
+  var j := 0;
+  while i < nums.Length
+    invariant j <= i
+    invariant i <= nums.Length
+    invariant old(nums[i..]) == nums[i..];
+    invariant multiset(nums[..j]) == multiset(old(nums[..i]))[val := 0]
+  {
+    if nums[i] != val {
+      nums[j] := nums[i];
+      j := j + 1;
+      assert nums[..j] == nums[..j-1] + [nums[i]];
     }
-    assert old(nums[..i]) == old(nums[..]);
-    return j;
+    i := i + 1;
+  }
+  assert old(nums[..i]) == old(nums[..]);
+  return j;
 }
diff --git a/leetcode/0121-stocks.dfy b/leetcode/0121-stocks.dfy
index 026832e..e0fabea 100644
--- a/leetcode/0121-stocks.dfy
+++ b/leetcode/0121-stocks.dfy
@@ -5,7 +5,7 @@
 //   if a >= b then a else b
 // }
 
-function method Max(a: int, b: int): int {
+function Max(a: int, b: int): int {
   if a >= b then a else b
 }
 
diff --git a/leetcode/0155-min-stack.dfy b/leetcode/0155-min-stack.dfy
index 1a2e526..7841a3a 100644
--- a/leetcode/0155-min-stack.dfy
+++ b/leetcode/0155-min-stack.dfy
@@ -17,7 +17,7 @@ class MinStack {
   ghost var dataSeq: seq<int>
   ghost var minsSeq: seq<int>
 
-  predicate Valid() 
+  ghost predicate Valid() 
     reads this
   {
     ToSeq(data) == dataSeq && ToSeq(mins) == minsSeq && |dataSeq| == |minsSeq|
@@ -33,7 +33,7 @@ class MinStack {
     minsSeq := [];
   }
 
-  predicate method IsEmpty()
+  predicate IsEmpty()
     reads this
     requires Valid()
     ensures IsEmpty() <==> |dataSeq| == 0
diff --git a/leetcode/0167-two-sum-ii.dfy b/leetcode/0167-two-sum-ii.dfy
index bdecac2..b37ffd8 100644
--- a/leetcode/0167-two-sum-ii.dfy
+++ b/leetcode/0167-two-sum-ii.dfy
@@ -3,7 +3,7 @@ include "../lib/Seq.dfy"
 
 import opened Seq
 
-function method TwoSumF(numbers: seq<int>, target: int, left: int, right: int) : (int, int)
+function TwoSumF(numbers: seq<int>, target: int, left: int, right: int) : (int, int)
 requires 0 <= left <= right < |numbers|;
 requires Sorted(numbers);
 decreases right - left;
diff --git a/leetcode/0226-invert-binary-tree.dfy b/leetcode/0226-invert-binary-tree.dfy
index 1dc822f..0eb74d1 100644
--- a/leetcode/0226-invert-binary-tree.dfy
+++ b/leetcode/0226-invert-binary-tree.dfy
@@ -3,7 +3,7 @@ include "../lib/adt/BinaryTree.dfy"
 
 import opened BinaryTree
 
-function method Mirror<T>(t: Tree<T>) : Tree<T>
+function Mirror<T>(t: Tree<T>) : Tree<T>
 {
     match t
     case Nil => Nil
diff --git a/lib/MinMax.dfy b/lib/MinMax.dfy
index 5af641f..54c2369 100644
--- a/lib/MinMax.dfy
+++ b/lib/MinMax.dfy
@@ -1,10 +1,10 @@
 module MinMax {
 
-  function method Min(a: int, b: int): int {
+  function Min(a: int, b: int): int {
     if a <= b then a else b
   }
 
-  function method Max(a: int, b: int): int {
+  function Max(a: int, b: int): int {
     if a >= b then a else b
   }
 
@@ -29,5 +29,5 @@ module MinMax {
     ensures a == b
   {
   }
-  
+
 }
\ No newline at end of file
diff --git a/lib/Pow.dfy b/lib/Pow.dfy
index 1868a61..f030181 100644
--- a/lib/Pow.dfy
+++ b/lib/Pow.dfy
@@ -43,6 +43,12 @@ module PowModule {
   lemma PowMul(x: int, y: int, e: nat)
     ensures Pow(x * y, e) == Pow(x, e) * Pow(y, e)
   {
+    if e == 0 {
+
+    }
+    else {
+      assert Pow(x*y, e-1) == Pow(x,e-1)*Pow(y,e-1);
+    }
   }
 
   lemma PowExpAdd(x: int, a: nat, b: nat)
@@ -53,10 +59,10 @@ module PowModule {
     }
   }
 
-  function method FastPow(b: int, e: nat): int
+  function FastPow(b: int, e: nat): int
     decreases e
   {
-    if e == 0 then 1 
+    if e == 0 then 1
     else if e % 2 == 0 then FastPow(b * b, e / 2)
     else b * FastPow(b, e - 1)
   }
diff --git a/lib/Seq.dfy b/lib/Seq.dfy
index 19ca143..335735f 100644
--- a/lib/Seq.dfy
+++ b/lib/Seq.dfy
@@ -2,18 +2,26 @@ module Seq {
 
   /***** Last *****/
 
-  function method Last<T>(xs: seq<T>): T
+  function Last<T>(xs: seq<T>): T
     requires 0 < |xs|
   {
     xs[|xs| - 1]
   }
 
-  function method RemoveLast<T>(xs: seq<T>): seq<T>
+  function RemoveLast<T>(xs: seq<T>): seq<T>
     requires 0 < |xs|
   {
     xs[..|xs| - 1]
   }
 
+  lemma LastAppend<T>(xs: seq<T>, x: T)
+    ensures Last(xs + [x]) == x
+  {}
+
+  lemma RemoveLastAppend<T>(xs: seq<T>, x: T)
+    ensures RemoveLast(xs + [x]) == xs
+  {}
+
   lemma ConcatRemoveLastLast<T>(xs: seq<T>)
     requires 0 < |xs|
     ensures RemoveLast(xs) + [Last(xs)] == xs
@@ -107,10 +115,12 @@ module Seq {
     }
   }
 
+
   lemma FoldlEq<A, B>(f: (A, B) -> A, z: A, xs: seq<B>)
     ensures Foldl'(f, z, xs) == Foldl(f, z, xs)
   {
     if |xs| > 0 {
+      FoldlEq(f, Foldl'(f, z, xs[..|xs| - 1]), xs[1..]);
       calc {
         Foldl(f, z, xs);
         { assert xs == xs[..|xs| - 1] + [xs[|xs| - 1]]; }
@@ -136,6 +146,7 @@ module Seq {
     }
   }
 
+
   function Sum(xs: seq<int>): int {
     Foldl'((a, b) => a + b, 0, xs)
   }
@@ -151,7 +162,7 @@ module Seq {
     }
   }
 
-  // method FilterMethod(xs: seq<int>, f: int -> bool) returns (ys: seq<int>) 
+  // method FilterMethod(xs: seq<int>, f: int -> bool) returns (ys: seq<int>)
   //   ensures forall y :: y in ys ==> f(y)
   //   ensures forall x :: x in xs && f(x) ==> x in ys
   // {
@@ -173,7 +184,7 @@ module Seq {
   //   ensures forall y :: y in Filter(xs, f) ==> f(y)
   //   ensures forall x :: x in xs && f(x) ==> x in Filter(xs, f)
   // {
-  //   if |xs| == 0 then [] 
+  //   if |xs| == 0 then []
   //   else if f(xs[0]) then [xs[0]] + Filter(xs[1..], f)
   //   else Filter(xs[1..], f)
   // }
@@ -188,7 +199,7 @@ module Seq {
     forall i :: 0 <= i < |xs| - 1 ==> xs[i] <= xs[i + 1]
   }
 
-  lemma SortedEq1(xs: seq<int>) 
+  lemma SortedEq1(xs: seq<int>)
     ensures Sorted(xs) <==> Sorted1(xs)
   {
     if |xs| > 0 {
@@ -207,7 +218,7 @@ module Seq {
     forall i :: 0 <= i < |xs| - 1 ==> xs[i] < xs[i + 1]
   }
 
-  lemma SortedStrictEq1(xs: seq<int>) 
+  lemma SortedStrictEq1(xs: seq<int>)
     ensures SortedStrict(xs) <==> SortedStrict1(xs)
   {
     if |xs| > 0 {
@@ -218,21 +229,21 @@ module Seq {
     }
   }
 
-  predicate IsSuffix<T>(xs: seq<T>, ys: seq<T>) {
+  predicate IsSuffix<T(==)>(xs: seq<T>, ys: seq<T>) {
     |xs| <= |ys| && xs == ys[|ys| - |xs|..]
   }
 
   /***** Distinct *****/
 
-  predicate Distinct<T>(xs: seq<T>) {
+  predicate Distinct<T(==)>(xs: seq<T>) {
     forall i, j :: 0 <= i < j < |xs| ==> xs[i] != xs[j]
   }
 
-  predicate DistinctRec<T>(xs: seq<T>) {
+  predicate DistinctRec<T(==)>(xs: seq<T>) {
     if |xs| == 0 then true else xs[0] !in xs[1..] && DistinctRec(xs[1..])
   }
 
-  predicate DistinctRecLast<T>(xs: seq<T>) {
+  predicate DistinctRecLast<T(==)>(xs: seq<T>) {
     if |xs| == 0 then true else Last(xs) !in RemoveLast(xs) && DistinctRecLast(RemoveLast(xs))
   }
 
diff --git a/lib/SeqMethods.dfy b/lib/SeqMethods.dfy
index eadb09c..39fffa5 100644
--- a/lib/SeqMethods.dfy
+++ b/lib/SeqMethods.dfy
@@ -47,7 +47,7 @@ module SeqMethods {
     return a;
   }
 
-  method FoldlIter<A, B>(f: (A, B) -> A, z: A, xs: seq<B>) returns (r: A) 
+  method FoldlIter<A, B>(f: (A, B) -> A, z: A, xs: seq<B>) returns (r: A)
     ensures r == Foldl'(f, z, xs)
     ensures r == Foldl(f, z, xs)
   {
diff --git a/lib/adt/BinaryTree.dfy b/lib/adt/BinaryTree.dfy
index 514f201..042a98f 100644
--- a/lib/adt/BinaryTree.dfy
+++ b/lib/adt/BinaryTree.dfy
@@ -3,138 +3,138 @@
 include "../seq/Count.dfy"
 
 module BinaryTree {
-    import opened SeqCount
-
-    datatype Tree<T> = Nil | Node(value: T, left: Tree<T>, right: Tree<T>)
-
-    predicate Member?<T>(x: T, t: Tree<T>) {
-        match t
-        case Nil => false
-        case Node(y, l, r) => x == y || Member?(x, l) || Member?(x, r)
-    }
-
-    function Size<T>(t: Tree<T>) : nat {
-        match t
-        case Nil => 0
-        case Node(_, l, r) => 1 + Size(l) + Size(r)
-    }
-
-    function Depth<T>(t: Tree<T>) : nat {
-        match t
-        case Nil => 0
-        case Node(_, l, r) => 1 + (if Depth(l) > Depth(r) then Depth(l) else Depth(r))
-    }
-
-    predicate Equal?<T>(t1: Tree<T>, t2: Tree<T>) {
-        match t1
-        case Nil => t2.Nil?
-        case Node(v1, l1, r1) =>
-            match t2
-            case Nil => false
-            case Node(v2, l2, r2) => v1 == v2 && Equal?(l1, l2) && Equal?(r1, r2)
-    }
-
-    lemma TreeIdentityEqual<T>(t: Tree<T>)
+  import opened SeqCount
+
+  datatype Tree<T> = Nil | Node(value: T, left: Tree<T>, right: Tree<T>)
+
+  predicate Member?<T(==)>(x: T, t: Tree<T>) {
+    match t
+    case Nil => false
+    case Node(y, l, r) => x == y || Member?(x, l) || Member?(x, r)
+  }
+
+  function Size<T>(t: Tree<T>) : nat {
+    match t
+    case Nil => 0
+    case Node(_, l, r) => 1 + Size(l) + Size(r)
+  }
+
+  function Depth<T>(t: Tree<T>) : nat {
+    match t
+    case Nil => 0
+    case Node(_, l, r) => 1 + (if Depth(l) > Depth(r) then Depth(l) else Depth(r))
+  }
+
+  predicate Equal?<T(==)>(t1: Tree<T>, t2: Tree<T>) {
+    match t1
+    case Nil => t2.Nil?
+    case Node(v1, l1, r1) =>
+      match t2
+      case Nil => false
+      case Node(v2, l2, r2) => v1 == v2 && Equal?(l1, l2) && Equal?(r1, r2)
+  }
+
+  lemma TreeIdentityEqual<T>(t: Tree<T>)
     ensures Equal?(t, t)
-    {
-    }
+  {
+  }
 
-    lemma NilNotEqNode<T>(t1: Tree<T>, t2: Tree<T>)
+  lemma NilNotEqNode<T>(t1: Tree<T>, t2: Tree<T>)
     ensures t1.Nil? && t2.Node? ==> !Equal?(t1, t2)
-    {
-    }
+  {
+  }
 
-    predicate IsLeaf?<T>(t: Tree<T>) {
-        t.Node? && t.left.Nil? && t.right.Nil?
-    }
+  predicate IsLeaf?<T>(t: Tree<T>) {
+    t.Node? && t.left.Nil? && t.right.Nil?
+  }
 
-    lemma LeafNodeEqual<T>(t1: Tree<T>, t2: Tree<T>)
+  lemma LeafNodeEqual<T>(t1: Tree<T>, t2: Tree<T>)
     ensures IsLeaf?(t1) && IsLeaf?(t2) && t1.value == t2.value ==> Equal?(t1, t2)
-    {
-    }
+  {
+  }
 
-    function CountBT<T>(x: T, t: Tree<T>): nat {
-        match t
-        case Nil => 0
-        case Node(y, l, r) =>
-            (if x == y then 1 else 0) + CountBT(x, l) + CountBT(x, r)
-    }
+  function CountBT<T(==)>(x: T, t: Tree<T>): nat {
+    match t
+    case Nil => 0
+    case Node(y, l, r) =>
+      (if x == y then 1 else 0) + CountBT(x, l) + CountBT(x, r)
+  }
 
-    lemma EqualImpSameCount<T>(t1: Tree<T>, t2: Tree<T>)
+  lemma EqualImpSameCount<T>(t1: Tree<T>, t2: Tree<T>)
     requires Equal?(t1, t2)
     ensures forall x :: CountBT(x, t1) == CountBT(x, t2)
-    {
-    }
+  {
+  }
 
-    lemma EqualImpSameCountImp<T>(t1: Tree<T>, t2: Tree<T>)
+  lemma EqualImpSameCountImp<T>(t1: Tree<T>, t2: Tree<T>)
     ensures Equal?(t1, t2) ==> forall x :: CountBT(x, t1) == CountBT(x, t2)
-    {
-        if Equal?(t1, t2) {
-            EqualImpSameCount(t1, t2);
-        }
+  {
+    if Equal?(t1, t2) {
+      EqualImpSameCount(t1, t2);
     }
+  }
 
-    lemma MemberCountGE1<T>(x : T, t: Tree<T>)
+  lemma MemberCountGE1<T>(x : T, t: Tree<T>)
     ensures Member?(x, t) ==> CountBT(x, t) >= 1
-    {
-    }
+  {
+  }
 
-    function ToMS<T>(t: Tree<T>): multiset<T> {
-        match t
-        case Nil => multiset{}
-        case Node(x, l, r) => multiset{x} + ToMS(l) + ToMS(r)
-    }
+  function ToMS<T>(t: Tree<T>): multiset<T> {
+    match t
+    case Nil => multiset{}
+    case Node(x, l, r) => multiset{x} + ToMS(l) + ToMS(r)
+  }
 
-    lemma MemberInToMS<T>(x: T, t: Tree<T>)
+  lemma MemberInToMS<T>(x: T, t: Tree<T>)
     ensures Member?(x, t) ==> x in ToMS(t)
-    {
-    }
-    
-    function InorderFlatten<T>(t: Tree<T>) : seq<T>
-    {
-        match t
-        case Nil => []
-        case Node(x, l, r) => InorderFlatten(l) + [x] + InorderFlatten(r)
-    }
+  {
+  }
+
+  function InorderFlatten<T>(t: Tree<T>) : seq<T>
+  {
+    match t
+    case Nil => []
+    case Node(x, l, r) => InorderFlatten(l) + [x] + InorderFlatten(r)
+  }
 
-    lemma NotMemberCount0<T>(t: Tree<T>)
+  lemma NotMemberCount0<T>(t: Tree<T>)
     ensures forall x :: !Member?(x, t) <==> CountBT(x, t) == 0
-    {
+  {
 
-    }
+  }
 
-    lemma NotMemberBTEqNotMemberIOFlatten<T>(t: Tree<T>)
+  lemma NotMemberBTEqNotMemberIOFlatten<T>(t: Tree<T>)
     ensures forall x :: !Member?(x, t) <==> x !in InorderFlatten(t)
-    {
+  {
 
-    }
+  }
 
-    lemma PreorderFlattenPerm<T>(x: T, t: Tree<T>)
+  lemma PreorderFlattenPerm<T>(x: T, t: Tree<T>)
     ensures CountBT(x, t) == Count(PreorderFlatten(t), x)
-    {
-        match t {
-            case Nil => assert forall x :: CountBT(x, t) == Count(PreorderFlatten(t), x);
-            case Node(y, l , r) => {
-                var lf := PreorderFlatten(l);
-                var rf := PreorderFlatten(r);
-                var f := PreorderFlatten(t);
-                assert f == [y] + (lf + rf);
-                CountConcat(lf, rf, x);
-            }
-        }
-    }
-
-    function PreorderFlatten<T>(t: Tree<T>) : seq<T>
-    {
-        match t
-        case Nil => []
-        case Node(x, l, r) => [x] + PreorderFlatten(l) + PreorderFlatten(r)
-    }
-
-    function PostorderFlatten<T>(t: Tree<T>) : seq<T>
-    {
-        match t
-        case Nil => []
-        case Node(x, l, r) => PostorderFlatten(l) + PostorderFlatten(r) + [x]
-    }
+  {
+    match t {
+      case Nil => assert forall x :: CountBT(x, t) == Count(PreorderFlatten(t), x);
+      case Node(y, l , r) => {
+        var lf := PreorderFlatten(l);
+        var rf := PreorderFlatten(r);
+        var f := PreorderFlatten(t);
+        assert f == [y] + (lf + rf);
+        CountConcat(lf, rf, x);
+      }
+    }
+  }
+
+  function PreorderFlatten<T>(t: Tree<T>) : seq<T>
+  {
+    match t
+    case Nil => []
+    case Node(x, l, r) => [x] + PreorderFlatten(l) + PreorderFlatten(r)
+  }
+
+  function PostorderFlatten<T>(t: Tree<T>) : seq<T>
+  {
+    match t
+    case Nil => []
+    case Node(x, l, r) => PostorderFlatten(l) + PostorderFlatten(r) + [x]
+  }
 }
\ No newline at end of file
diff --git a/lib/math/Abs.dfy b/lib/math/Abs.dfy
index 2b6c418..26f305e 100644
--- a/lib/math/Abs.dfy
+++ b/lib/math/Abs.dfy
@@ -1,6 +1,6 @@
 include "DivMod.dfy"
 
-function method Abs(x: int): int {
+function Abs(x: int): int {
   if x < 0 then -x else x
 }
 
diff --git a/lib/math/EvenOdd.dfy b/lib/math/EvenOdd.dfy
index 7853418..df6de98 100644
--- a/lib/math/EvenOdd.dfy
+++ b/lib/math/EvenOdd.dfy
@@ -1,10 +1,10 @@
 module EvenOdd {
 
-  function method Even(n: int): bool {
+  function Even(n: int): bool {
     n % 2 == 0
   }
 
-  function method Odd(n: int): bool {
+  function Odd(n: int): bool {
     n % 2 != 0
   }
 
@@ -63,5 +63,5 @@ module EvenOdd {
   {
     assert n == 2 * (n / 2) + 1;
   }
-  
+
 }
\ No newline at end of file
diff --git a/lib/math/Factors.dfy b/lib/math/Factors.dfy
index 6e7b1d9..ea2d1ff 100644
--- a/lib/math/Factors.dfy
+++ b/lib/math/Factors.dfy
@@ -1,7 +1,7 @@
 include "../Seq.dfy"
 
 module FactorsModule {
-  
+
   import opened Seq
 
   function AllFactorsSet(n: int): set<int> {
@@ -65,7 +65,7 @@ module FactorsModule {
   {
   }
 
-  // function Factors2(n: int, d: int): seq<int> 
+  // function Factors2(n: int, d: int): seq<int>
   //   requires n >= 1
   // {
   //   Filter(seq(n, i => i + 1), d => d > 0 && n % d == 0)
diff --git a/lib/math/Gcd.dfy b/lib/math/Gcd.dfy
index 28147a1..fa5a3d7 100644
--- a/lib/math/Gcd.dfy
+++ b/lib/math/Gcd.dfy
@@ -1,6 +1,6 @@
 include "Abs.dfy"
 
-function method {:opaque} Gcd(a: int, b: int): int
+function {:opaque} Gcd(a: int, b: int): int
   decreases Abs(b)
 {
   if b != 0 then Gcd(b, a % b) else if a == 0 then 1 else Abs(a)
diff --git a/lib/seq/Count.dfy b/lib/seq/Count.dfy
index 669d2da..90a0e02 100644
--- a/lib/seq/Count.dfy
+++ b/lib/seq/Count.dfy
@@ -1,55 +1,54 @@
 include "../Seq.dfy"
 
 module SeqCount {
-import opened Seq
+  import opened Seq
 
-function Count<T>(xs: seq<T>, v: T): nat {
-  if |xs| == 0 then 0
-  else (if xs[0] == v then 1 else 0) + Count(xs[1..], v)
-}
-
-lemma Count0<T>(xs: seq<T>, v: T)
-  ensures Count(xs, v) == 0 <==> v !in xs
-{
-}
+  function Count<T(==)>(xs: seq<T>, v: T): nat {
+    if |xs| == 0 then 0
+    else (if xs[0] == v then 1 else 0) + Count(xs[1..], v)
+  }
 
-lemma CountPos<T>(xs: seq<T>, v: T)
-  ensures Count(xs, v) > 0 <==> v in xs
-{
-}
+  lemma Count0<T>(xs: seq<T>, v: T)
+    ensures Count(xs, v) == 0 <==> v !in xs
+  {
+  }
 
-lemma CountMultiset<T>(xs: seq<T>, v: T)
-  ensures Count(xs, v) == multiset(xs)[v]
-{
-  if |xs| > 0 {
-    assert xs == [xs[0]] + xs[1..];
+  lemma CountPos<T>(xs: seq<T>, v: T)
+    ensures Count(xs, v) > 0 <==> v in xs
+  {
   }
-}
 
-lemma CountConcat<T>(xs: seq<T>, ys: seq<T>, v: T)
-  ensures Count(xs + ys, v) == Count(xs, v) + Count(ys, v)
-{
-  calc {
-    Count(xs + ys, v);
-    { CountMultiset(xs + ys, v); }
-    multiset(xs + ys)[v];
-    multiset(xs)[v] + multiset(ys)[v];
-    { CountMultiset(xs, v); CountMultiset(ys, v); }
-    Count(xs, v) + Count(ys, v);
+  lemma CountMultiset<T>(xs: seq<T>, v: T)
+    ensures Count(xs, v) == multiset(xs)[v]
+  {
+    if |xs| > 0 {
+      assert xs == [xs[0]] + xs[1..];
+    }
   }
-}
 
-lemma CountFoldl<T>(xs: seq<T>, v: T)
-  ensures Count(xs, v) == Foldl'((r, x) => (if x == v then 1 else 0) + r, 0, xs)
-{
-  if |xs| > 0 {
+  lemma CountConcat<T>(xs: seq<T>, ys: seq<T>, v: T)
+    ensures Count(xs + ys, v) == Count(xs, v) + Count(ys, v)
+  {
     calc {
-      Count(xs, v);
-      { CountConcat(RemoveLast(xs), [Last(xs)], v); ConcatRemoveLastLast(xs); }
-      Count(RemoveLast(xs), v) + Count([Last(xs)], v);
-      Foldl'((r, x) => (if x == v then 1 else 0) + r, 0, RemoveLast(xs)) + (if Last(xs) == v then 1 else 0);
+      Count(xs + ys, v);
+      { CountMultiset(xs + ys, v); }
+      multiset(xs + ys)[v];
+      multiset(xs)[v] + multiset(ys)[v];
+      { CountMultiset(xs, v); CountMultiset(ys, v); }
+      Count(xs, v) + Count(ys, v);
+    }
+  }
+
+  lemma CountFoldl<T>(xs: seq<T>, v: T)
+    ensures Count(xs, v) == Foldl'((r, x) => (if x == v then 1 else 0) + r, 0, xs)
+  {
+    if |xs| > 0 {
+      calc {
+        Count(xs, v);
+        { CountConcat(RemoveLast(xs), [Last(xs)], v); ConcatRemoveLastLast(xs); }
+        Count(RemoveLast(xs), v) + Count([Last(xs)], v);
+        Foldl'((r, x) => (if x == v then 1 else 0) + r, 0, RemoveLast(xs)) + (if Last(xs) == v then 1 else 0);
+      }
     }
   }
 }
-}
-  
\ No newline at end of file
diff --git a/lib/seq/Digits.dfy b/lib/seq/Digits.dfy
index 1192561..7e8aa3b 100644
--- a/lib/seq/Digits.dfy
+++ b/lib/seq/Digits.dfy
@@ -7,8 +7,9 @@ module DigitsModule {
   import DivMod
 
   // Verification of all lemmas is faster with {:opaque}
-  function {:opaque} Digits(n: int, base: int): seq<int> 
+  function {:opaque} Digits(n: int, base: int): seq<int>
     requires 2 <= base
+    decreases n * 1
   {
     if n <= 0 then [0] else if n < base then [n] else Digits(n / base, base) + [n % base]
   }
@@ -21,22 +22,43 @@ module DigitsModule {
     reveal Digits();
   }
 
-  lemma DigitsBound(n: int, base: int, i: int)
+  lemma DigitsBound(n: int, base: int)
     requires 2 <= base
-    requires 0 <= i < |Digits(n, base)|
-    ensures 0 <= Digits(n, base)[i] < base
+    decreases n
+    ensures forall i :: 0 <= i < |Digits(n, base)| ==> 0 <= Digits(n, base)[i] < base
   {
     reveal Digits();
+    if n >= base {
+      assert n / base < n;
+      DigitsBound(n/base, base);
+      assert Digits(n,base) == Digits(n/base, base) + [n%base];
+    }
   }
 
   lemma DigitsSpec(n: int, base: int)
     requires 0 <= n && 2 <= base
     ensures Foldl'((r, d) => r * base + d, 0, Digits(n, base)) == n
+    decreases n
     // ensures Foldl((r, d) => r * base + d, 0, Digits(n, base)) == n
   {
     reveal Digits();
     if n >= base {
+      assert n / base < n;
       DigitsSpec(n / base, base);
+      assert |Digits(n / base, base) + [n % base]| >= 1;
+      assert RemoveLast(Digits(n / base, base) + [n % base]) == Digits(n / base, base) by {
+        RemoveLastAppend(Digits(n / base, base), n % base);
+      }
+      assert Last(Digits(n / base, base) + [n % base]) == n % base by {
+        LastAppend(Digits(n / base, base), n % base);
+      }
+      calc ==
+      {
+        Foldl'((r, d) => r * base + d, 0, Digits(n, base));
+        Foldl'((r, d) => r * base + d, 0, Digits(n / base, base) + [n % base]);
+        Foldl'((r, d) => r * base + d, 0, RemoveLast(Digits(n / base, base) + [n % base]))*base + Last(Digits(n / base, base) + [n % base]);
+        Foldl'((r, d) => r * base + d, 0, Digits(n / base, base))*base +  (n % base);
+      }
     }
     // FoldlEq((r, d) => r * base + d, 0, Digits(n, base));
   }
@@ -55,8 +77,15 @@ module DigitsModule {
     requires 0 < a
     ensures 0 < |Digits(a, base)|
     ensures 0 < Digits(a, base)[0]
+    decreases a
   {
     reveal Digits();
-  }
+    if a < base {
 
+    } else {
+      assert a / base < a;
+      DigitsNoLeading0(a/base, base);
+      assert Digits(a, base)[0] == Digits(a / base, base)[0];
+    }
+  }
 }
diff --git a/lib/seq/Fold.dfy b/lib/seq/Fold.dfy
index 9aa82ef..97a5a5c 100644
--- a/lib/seq/Fold.dfy
+++ b/lib/seq/Fold.dfy
@@ -1,10 +1,10 @@
-function method Last<T>(xs: seq<T>): T
+function Last<T>(xs: seq<T>): T
   requires 0 < |xs|
 {
   xs[|xs| - 1]
 }
 
-function method RemoveLast<T>(xs: seq<T>): seq<T>
+function RemoveLast<T>(xs: seq<T>): seq<T>
   requires 0 < |xs|
 {
   xs[..|xs| - 1]
@@ -78,19 +78,19 @@ function Foldr'<A, B>(f: (B, A) -> A, xs: seq<B>, z: A): A {
 //   }
 // }
 
-predicate OpComm<T>(f: (T, T) -> T, dom: seq<T>) {
+predicate OpComm<T(==)>(f: (T, T) -> T, dom: seq<T>) {
   forall x, y :: x in dom && y in dom ==> f(x, y) == f(y, x)
 }
 
-predicate OpAssoc<T(!new)>(f: (T, T) -> T) {
+ghost predicate OpAssoc<T(!new)>(f: (T, T) -> T) {
   forall x, y, z :: f(x, f(y, z)) == f(f(x, y), z)
 }
 
-predicate OpNeutral<T(!new)>(f: (T, T) -> T, z: T) {
+ghost predicate OpNeutral<T(!new)>(f: (T, T) -> T, z: T) {
   forall x :: f(x, z) == f(z, x) == x
 }
 
-lemma FoldrEqFoldl<T(!new)>(f: (T, T) -> T, xs: seq<T>, z: T) 
+lemma FoldrEqFoldl<T(!new)>(f: (T, T) -> T, xs: seq<T>, z: T)
   requires OpAssoc(f)
   requires OpNeutral(f, z)
   ensures Foldr(f, xs, z) == Foldl(f, z, xs)
diff --git a/lib/seq/Palindrome.dfy b/lib/seq/Palindrome.dfy
index cb5fcf7..89e41e0 100644
--- a/lib/seq/Palindrome.dfy
+++ b/lib/seq/Palindrome.dfy
@@ -5,34 +5,40 @@ include "../Seq.dfy"
 import opened Seq
 
 /***** Palindrome *****/
-predicate Palindrome?<T>(s: seq<T>) {
+predicate Palindrome?<T(==)>(s: seq<T>) {
   if |s| <= 1 then true else (s[0] == s[|s|-1] && Palindrome?(s[1..|s|-1]))
 }
 
 lemma OneCharStringIsPalindrome<T>(s: seq<T>)
-ensures |s| == 1 ==> Palindrome?(s)
+  ensures |s| == 1 ==> Palindrome?(s)
 {}
 
 lemma PalindromeIndex<T>(s: seq<T>)
-requires Palindrome?(s)
-ensures forall i :: 0 <= i < |s| ==> s[i] == s[|s|-1-i]
+  requires Palindrome?(s)
+  ensures forall i :: 0 <= i < |s| ==> s[i] == s[|s|-1-i]
 {
+  if |s| <= 1 {
+
+  }
 }
 
-lemma PalindromIndexImp<T>(s: seq<T>)
-ensures Palindrome?(s) ==> (forall i :: 0 <= i < |s| ==> s[i] == s[|s|-1-i])
+lemma PalindromeIndexRev<T>(s: seq<T>)
+  requires forall i :: 0 <= i < |s| ==> s[i] == s[|s|-1-i]
+  ensures Palindrome?(s)
+{}
+
+lemma PalindromImpliesReverseEq<T>(s: seq<T>)
+  requires Palindrome?(s)
+  ensures Reverse(s) == s
 {
-  if Palindrome?(s) {
-    PalindromeIndex(s);
-  }
+  ReverseIndexAll(s);
+  PalindromeIndex(s);
 }
 
-lemma PalindromRelReverse<T>(s: seq<T>)
-ensures Palindrome?(s) <==> Reverse(s) == s
+lemma ReverseEqImpliesPalindrom<T>(s: seq<T>)
+  requires Reverse(s) == s
+  ensures Palindrome?(s)
 {
-  if |s| > 1 {
-    var t := s[1..|s| - 1];
-    ReverseIndexAll(s);
-    ReverseIndexAll(t);
-  }
+  ReverseIndexAll(s);
+  PalindromeIndexRev(s);
 }
\ No newline at end of file
diff --git a/lib/seq/Subseq.dfy b/lib/seq/Subseq.dfy
index cd308fc..7c94ea0 100644
--- a/lib/seq/Subseq.dfy
+++ b/lib/seq/Subseq.dfy
@@ -2,7 +2,7 @@ include "../Seq.dfy"
 
 import opened Seq
 
-predicate {:opaque} Subseq<T>(xs: seq<T>, ys: seq<T>) {
+predicate {:opaque} Subseq<T(==)>(xs: seq<T>, ys: seq<T>) {
   if |xs| == 0 then true
   else if |ys| == 0 then false
   else if xs[0] == ys[0] then Subseq(xs[1..], ys[1..])
diff --git a/lib/seq/Undup.dfy b/lib/seq/Undup.dfy
index 713f4a7..bed77ac 100644
--- a/lib/seq/Undup.dfy
+++ b/lib/seq/Undup.dfy
@@ -2,7 +2,7 @@ include "../Seq.dfy"
 
 import opened Seq
 
-function {:opaque} Undup<T>(xs: seq<T>): seq<T> {
+function {:opaque} Undup<T(==)>(xs: seq<T>): seq<T> {
   if |xs| == 0 then xs 
   else if Last(xs) in RemoveLast(xs) then Undup(RemoveLast(xs))
   else Undup(RemoveLast(xs)) + [Last(xs)]
diff --git a/set_of_seq.dfy b/set_of_seq.dfy
index 9316427..c4e9ad8 100644
--- a/set_of_seq.dfy
+++ b/set_of_seq.dfy
@@ -1,6 +1,6 @@
 function set_of_seq<T>(s: seq<T>): set<T>
 {
-  set x: T | x in s :: x
+  set x: T | x in s
 }
 
 lemma in_set_of_seq<T>(x: T, s: seq<T>)
@@ -31,6 +31,12 @@ function set_of_seq_ind<T>(s: seq<T>): set<T>
 lemma set_of_seq_ind_eq<T>(s: seq<T>)
   ensures set_of_seq(s) == set_of_seq_ind(s)
 {
+  if s == [] {
+
+  } else {
+    assert (set x: T | x in s[1..]) == set_of_seq_ind(s[1..]);
+    assert (set x: T | x in s) == ({s[0]} + (set x: T | x in s[1..]));
+  }
 }
 
 lemma card_set_of_seq_le<T>(s: seq<T>)
@@ -40,16 +46,16 @@ lemma card_set_of_seq_le<T>(s: seq<T>)
   }
   else {
     calc {
-      |set_of_seq(s)|;
-      == { set_of_seq_ind_eq(s); }
-        |set_of_seq_ind(s)|;
-      == { assert s == [s[0]] + s[1..]; }
-        |set_of_seq_ind([s[0]] + s[1..])|;
-      <= 1 + |set_of_seq_ind(s[1..])|;
-      == { set_of_seq_ind_eq(s[1..]); }
-        1 + |set_of_seq(s[1..])|;
-      <= { card_set_of_seq_le(s[1..]); }
-        1 + |s[1..]|;
+       |set_of_seq(s)|;
+    == { set_of_seq_ind_eq(s); }
+       |set_of_seq_ind(s)|;
+    == { assert s == [s[0]] + s[1..]; }
+       |set_of_seq_ind([s[0]] + s[1..])|;
+    <= 1 + |set_of_seq_ind(s[1..])|;
+    == { set_of_seq_ind_eq(s[1..]); }
+       1 + |set_of_seq(s[1..])|;
+    <= { card_set_of_seq_le(s[1..]); }
+       1 + |s[1..]|;
     }
   }
 }
@@ -59,7 +65,7 @@ lemma set_of_seq_append<T>(s1: seq<T>, s2: seq<T>)
 {
 }
 
-function undup<T>(s: seq<T>): seq<T>
+function undup<T(==)>(s: seq<T>): seq<T>
 {
   if s == [] then
     []
@@ -80,9 +86,9 @@ lemma set_of_seq_undup<T>(s: seq<T>)
   if s == [] {
   }
   else {
-//    set_of_seq_ind_eq(undup(s));
-//    assert s == [s[0]] + s[1..];
-//    set_of_seq_ind_eq(undup(s[1..]));
+    //    set_of_seq_ind_eq(undup(s));
+    //    assert s == [s[0]] + s[1..];
+    //    set_of_seq_ind_eq(undup(s[1..]));
     calc {
       set_of_seq(undup(s));
       { set_of_seq_ind_eq(undup(s)); }
@@ -98,19 +104,19 @@ lemma undup_undup<T>(s: seq<T>)
 {
   if s == [] {
   }
-  else if s[0] in s[1..] {  
-//    assert s == [s[0]] + s[1..];
-//    set_of_seq_ind_eq(s);
-//    set_of_seq_ind_eq(s[1..]);
+  else if s[0] in s[1..] {
+    //    assert s == [s[0]] + s[1..];
+    //    set_of_seq_ind_eq(s);
+    //    set_of_seq_ind_eq(s[1..]);
   }
   else {
-//    assume undup(s[1..]) == undup(s)[1..];
+    //    assume undup(s[1..]) == undup(s)[1..];
     in_undup(s[0], s[1..]);
-//    assert s[0] !in undup(s[1..]);
+    //    assert s[0] !in undup(s[1..]);
   }
 }
 
-predicate subseq<T>(s1: seq<T>, s2: seq<T>)
+predicate subseq<T(==)>(s1: seq<T>, s2: seq<T>)
 {
   if s1 == [] then
     true
@@ -155,7 +161,7 @@ lemma in_subseq<T>(x: T, s1: seq<T>, s2: seq<T>)
 {
 }
 
-predicate uniq_ind<T>(s: seq<T>)
+predicate uniq_ind<T(==)>(s: seq<T>)
 {
   if s == [] then
     true
@@ -217,10 +223,10 @@ lemma card_set_of_seq_uniq<T>(s: seq<T>)
     set_of_seq_ind_eq(s[1..]);
     set_of_seq_ind_eq(s);
   }
-    
-//  undup_uniq(s);
-//  set_of_seq_ind_eq(s);
-//  card_set_of_undup(s);
+
+  //  undup_uniq(s);
+  //  set_of_seq_ind_eq(s);
+  //  card_set_of_undup(s);
 }
 
 lemma card_set_of_undup<T>(s: seq<T>)
diff --git a/test_modules.dfy b/test_modules.dfy
index 7a1a67b..f38dde1 100644
--- a/test_modules.dfy
+++ b/test_modules.dfy
@@ -4,14 +4,14 @@ module Random {
     ensures a <= r <= b
 }
 
-function method rand(n: int): int
+function rand(n: int): int
   requires 0 <= n
   ensures 0 <= rand(n) <= n
 
 method rand2(n: int) returns (r: int)
   requires 0 <= n
   ensures 0 <= r <= n
-  
+
 method Main()
 {
   var x := 2;
@@ -19,7 +19,7 @@ method Main()
 
   var r1 := Random.random(x, y);
   var r2 := Random.random(x, y);
-  
+
   assert r1 <= 4 && r2 <= 4;
 
   r1 := rand(y);
diff --git a/test_shuffle.dfy b/test_shuffle.dfy
index 1bb0c29..fbd9062 100644
--- a/test_shuffle.dfy
+++ b/test_shuffle.dfy
@@ -1,6 +1,6 @@
 
 method random(a: int, b: int) returns (r: int)
-//  requires a <= b
+  //  requires a <= b
   ensures a <= b ==> a <= r <= b
 
 lemma eqMultiset_t<T>(t: T, s1: seq<T>, s2: seq<T>)
@@ -11,17 +11,17 @@ lemma eqMultiset_t<T>(t: T, s1: seq<T>, s2: seq<T>)
     t in s1;
     t in multiset(s1);
     // Not necessary:
-//    t in multiset(s2);
-//    t in s2;
+    //    t in multiset(s2);
+    //    t in s2;
   }
-/*  
-  if (t in s1) {
-    assert t in multiset(s1);
-  }
-  else {
-    assert t !in multiset(s1);
-  }
-*/
+  /*  
+    if (t in s1) {
+      assert t in multiset(s1);
+    }
+    else {
+      assert t !in multiset(s1);
+    }
+  */
 }
 
 lemma eqMultiset<T>(s1: seq<T>, s2: seq<T>)
@@ -46,7 +46,7 @@ method swap<T>(a: array<T>, i: int, j: int)
   a[i] := a[j];
   a[j] := t;
 }
-  
+
 method getAllShuffledDataEntries<T(0)>(m_dataEntries: array<T>) returns (result: array<T>)
   // requires m_dataEntries != null
   // ensures result != null
@@ -59,7 +59,7 @@ method getAllShuffledDataEntries<T(0)>(m_dataEntries: array<T>) returns (result:
   }
 
   assert result[..] == m_dataEntries[..];
-  
+
   var k := result.Length - 1;
   while (k >= 0)
     invariant multiset(result[..]) == multiset(m_dataEntries[..])
@@ -70,7 +70,7 @@ method getAllShuffledDataEntries<T(0)>(m_dataEntries: array<T>) returns (result:
     if (i != k) {
       swap(result, i, k);
     }
-    
+
     k := k - 1;
   }
 }
@@ -86,11 +86,11 @@ lemma in_set_of_seq<T>(x: T, s: seq<T>)
 lemma subset_set_of_seq<T>(s1: seq<T>, s2: seq<T>)
   requires set_of_seq(s1) <= set_of_seq(s2)
   ensures forall x :: x in s1 ==> x in s2
-  
+
 method getRandomDataEntry<T(==)>(m_workList: array<T>, avoidSet: seq<T>) returns (e: T)
   requires m_workList.Length > 0
-//  ensures set_of_seq(avoidSet) < set_of_seq(m_workList[..]) ==> e !in avoidSet
-//  ensures avoidSet < m_workList[..] ==> e in m_workList[..]
+  //  ensures set_of_seq(avoidSet) < set_of_seq(m_workList[..]) ==> e !in avoidSet
+  //  ensures avoidSet < m_workList[..] ==> e in m_workList[..]
 {
   var k := m_workList.Length - 1;
 
@@ -103,9 +103,9 @@ method getRandomDataEntry<T(==)>(m_workList: array<T>, avoidSet: seq<T>) returns
     if (e !in avoidSet) {
       return e;
     }
-    
+
     k := k - 1;
   }
-  
+
   return m_workList[0];
 }
diff --git a/uniq.dfy b/uniq.dfy
index a17acdd..177f7f2 100644
--- a/uniq.dfy
+++ b/uniq.dfy
@@ -1,19 +1,19 @@
-predicate uniq_mult1<T>(s: seq<T>)
+predicate uniq_mult1<T(==)>(s: seq<T>)
 {
   forall t :: t in s ==> multiset(s)[t] == 1
 }
 
-predicate uniq_mult2<T>(s: seq<T>)
+predicate uniq_mult2<T(==)>(s: seq<T>)
 {
   forall t :: t in s ==> multiset(s)[t] <= 1
 }
 
-predicate uniq_distinct<T>(s: seq<T>)
+predicate uniq_distinct<T(==)>(s: seq<T>)
 {
   forall i, j :: 0 <= i < |s| && 0 <= j < |s| && i != j ==> s[i] != s[j]
 }
 
-predicate uniq_ind<T>(s: seq<T>)
+predicate uniq_ind<T(==)>(s: seq<T>)
 {
   if s == [] then true else s[0] !in s[1..] && uniq_ind(s[1..])
 }
@@ -28,7 +28,7 @@ lemma lemma2<T>(s: seq<T>)
 {
 }
 
-function count_eq<T>(x: T, s: seq<T>): nat
+function count_eq<T(==)>(x: T, s: seq<T>): nat
 {
   if s == [] then
     0
@@ -65,7 +65,7 @@ lemma uniq_count<T>(x: T, s: seq<T>)
     }
   }
   else {
-//    uniq_count(x, s[1..]);
+    //    uniq_count(x, s[1..]);
   }
 }
 
@@ -124,16 +124,16 @@ lemma in_uniq_append<T>(x: T, s1: seq<T>, s2: seq<T>)
       false;
     }
   }
-/*
-  if x in s1 {
-    var i :| 0 <= i < |s1| && s1[i] == x;
-    if x in s2 {
-      var j :| 0 <= j < |s2| && s2[j] == x;
-      assert (s1 + s2)[|s1| + j] == x;
-      lemma1(s1 + s2);
+  /*
+    if x in s1 {
+      var i :| 0 <= i < |s1| && s1[i] == x;
+      if x in s2 {
+        var j :| 0 <= j < |s2| && s2[j] == x;
+        assert (s1 + s2)[|s1| + j] == x;
+        lemma1(s1 + s2);
+      }
     }
-  }
-*/
+  */
 }
 
 lemma uniq_sub_aux<T>(x: T, s: seq<T>, a: int, b: int)
@@ -194,13 +194,13 @@ lemma count_multiset<T>(x: T, s: seq<T>)
   }
   else {
     assert s == [s[0]] + s[1..];
-//    calc {
-//      count_eq(x, s);
-//      (if x == s[0] then 1 else 0) + count_eq(x, s[1..]);
-//      multiset{s[0]}[x] + multiset(s[1..])[x];
-//      { assert s == [s[0]] + s[1..]; }
-//      multiset(s)[x];
-//    }
+    //    calc {
+    //      count_eq(x, s);
+    //      (if x == s[0] then 1 else 0) + count_eq(x, s[1..]);
+    //      multiset{s[0]}[x] + multiset(s[1..])[x];
+    //      { assert s == [s[0]] + s[1..]; }
+    //      multiset(s)[x];
+    //    }
   }
 }
 
@@ -237,8 +237,8 @@ lemma lemma3<T>(s: seq<T>)
 lemma lemma_all<T>(s: seq<T>)
   ensures uniq_ind(s) == uniq_distinct(s) == uniq_mult1(s) == uniq_mult2(s)
 {
-//  lemma1(s);
-//  lemma2(s);
+  //  lemma1(s);
+  //  lemma2(s);
   lemma3(s);
 }
 
diff --git a/vector.dfy b/vector.dfy
index 29100ae..9e3865b 100644
--- a/vector.dfy
+++ b/vector.dfy
@@ -27,19 +27,19 @@ module Vec {
   class Vector<T(0)> {
     ghost var Contents: seq<T>;
     ghost var Repr: set<object>;
-    
+
     var objs: array<T>;
     var capacity: int;
     var length: int;
-      
-    predicate Valid()
+
+    ghost predicate Valid()
       reads this, objs
     {
-      this in Repr && objs in Repr && 
-        capacity == objs.Length &&
-        0 <= length <= capacity &&
-        1 <= capacity &&
-        Contents == objs[..length]
+      this in Repr && objs in Repr &&
+      capacity == objs.Length &&
+      0 <= length <= capacity &&
+      1 <= capacity &&
+      Contents == objs[..length]
     }
 
     constructor ()
@@ -112,7 +112,7 @@ module Vec {
         assert capacity > length;
         assert objs.Length == capacity;
         assert objs.Length > length;
-        
+
         objs[length] := obj;
         length := length + 1;
       }