diff --git a/audit.log b/audit.log
index 6777b8da..ffd63227 100644
--- a/audit.log
+++ b/audit.log
@@ -1,7 +1,2 @@
-src/Distributions/Uniform/Correctness.dfy(31,17): UniformFullCorrectness: Declaration has explicit `{:axiom}` attribute. 
-src/Distributions/Uniform/Model.dfy(19,33): Sample: Declaration has explicit `{:axiom}` attribute. 
-src/Distributions/Uniform/Model.dfy(46,17): IntervalSampleIsMeasurePreserving: Declaration has explicit `{:axiom}` attribute. 
-src/ProbabilisticProgramming/Independence.dfy(30,27): IsIndep: Declaration has explicit `{:axiom}` attribute. 
-src/ProbabilisticProgramming/Independence.dfy(70,17): IsIndepImpliesIsIndepFunction: Declaration has explicit `{:axiom}` attribute. 
-src/ProbabilisticProgramming/Independence.dfy(74,17): MapIsIndep: Declaration has explicit `{:axiom}` attribute. 
+src/Distributions/Uniform/Model.dfy(19,26): Sample: Declaration has explicit `{:axiom}` attribute. 
 src/ProbabilisticProgramming/RandomSource.dfy(50,17): ProbIsProbabilityMeasure: Declaration has explicit `{:axiom}` attribute. 
diff --git a/src/Distributions/Uniform/Correctness.dfy b/src/Distributions/Uniform/Correctness.dfy
index ca2dc0c7..1447f2c4 100644
--- a/src/Distributions/Uniform/Correctness.dfy
+++ b/src/Distributions/Uniform/Correctness.dfy
@@ -16,6 +16,17 @@ module Uniform.Correctness {
    Definitions
   ************/
 
+  function IntervalSampleIsIndepFunctionHelper(a: int, x: int): nat
+    requires x-a >= 0
+  {
+    x-a
+  }
+
+  ghost function IntervalSampleIsIndepFunctionHelperLifted(a: int, A: iset<int>): iset<nat>
+  {
+    iset x: int | x in A && x-a >= 0 :: IntervalSampleIsIndepFunctionHelper(a, x)
+  }
+
   ghost function SampleEquals(n: nat, i: nat): iset<Rand.Bitstream>
     requires 0 <= i < n
   {
@@ -28,10 +39,13 @@ module Uniform.Correctness {
 
   // Correctness theorem for Model.Sample
   // Equation (4.12) / PROB_BERN_UNIFORM
-  lemma {:axiom} UniformFullCorrectness(n: nat, i: nat)
+  lemma UniformFullCorrectness(n: nat, i: nat)
     requires 0 <= i < n
-    ensures SampleEquals(n, i) in Rand.eventSpace
-    ensures Rand.prob(SampleEquals(n, i)) == 1.0 / (n as real)
+    ensures
+      var e := iset s | Model.Sample(n)(s).Equals(i);
+      e in Rand.eventSpace &&
+      Rand.prob(e) == 1.0 / (n as real)
+  {}
 
   // Correctness theorem for Model.IntervalSample
   lemma UniformFullIntervalCorrectness(a: int, b: int, i: int)
@@ -55,17 +69,96 @@ module Uniform.Correctness {
     }
   }
 
-  // Equation (4.10)
-  lemma SampleIsIndep(n: nat)
+  lemma SampleIsIndepFunction(n: nat)
+    requires n > 0
+    ensures Independence.IsIndepFunction(Model.Sample(n))
+  {}
+
+  lemma IntervalSampleIsIndepFunction(a: int, b: int)
+    requires a < b
+    ensures Independence.IsIndepFunction(Model.IntervalSample(a, b))
+  {
+    forall A: iset<int>, E: iset<Rand.Bitstream> | E in Rand.eventSpace ensures Independence.IsIndepFunctionCondition(Model.IntervalSample(a, b), A, E) {
+      var A': iset<nat> := IntervalSampleIsIndepFunctionHelperLifted(a, A);
+      assert Measures.AreIndepEvents(Rand.eventSpace, Rand.prob, Monad.BitstreamsWithValueIn(Model.IntervalSample(a, b), A), Monad.BitstreamsWithRestIn(Model.IntervalSample(a, b), E)) by {
+        assert Monad.BitstreamsWithValueIn(Model.IntervalSample(a, b), A) == Monad.BitstreamsWithValueIn(Model.Sample(b - a), A') by {
+          forall s ensures s in Monad.BitstreamsWithValueIn(Model.IntervalSample(a, b), A) <==> s in Monad.BitstreamsWithValueIn(Model.Sample(b - a), A') {
+            calc {
+              s in Monad.BitstreamsWithValueIn(Model.IntervalSample(a, b), A);
+              Monad.Map(Model.Sample(b - a), x => a + x)(s).value in A;
+              Monad.Bind(Model.Sample(b - a), x => Monad.Return(a+x))(s).value in A;
+              Model.Sample(b - a)(s).value + a in A;
+              Model.Sample(b - a)(s).value in A';
+              s in Monad.BitstreamsWithValueIn(Model.Sample(b - a), A');
+            }
+          }
+        }
+        assert Monad.BitstreamsWithRestIn(Model.IntervalSample(a, b), E) == Monad.BitstreamsWithRestIn(Model.Sample(b-a), E) by {
+          forall s ensures s in Monad.BitstreamsWithRestIn(Model.IntervalSample(a, b), E) <==> s in Monad.BitstreamsWithRestIn(Model.Sample(b-a), E) {
+            calc {
+              s in Monad.BitstreamsWithRestIn(Model.IntervalSample(a, b), E);
+              Monad.Map(Model.Sample(b - a), x => a + x)(s).rest in E;
+              Monad.Bind(Model.Sample(b - a), x => Monad.Return(a+x))(s).rest in E;
+              Model.Sample(b-a)(s).rest in E;
+              s in Monad.BitstreamsWithRestIn(Model.Sample(b-a), E);
+            }
+          }
+        }
+        assert Independence.IsIndepFunctionCondition(Model.Sample(b - a), A', E) by {
+          SampleIsIndepFunction(b-a);
+        }
+      }
+    }
+  }
+
+  lemma SampleBound(n: nat, s: Rand.Bitstream)
     requires n > 0
-    ensures Independence.IsIndep(Model.Sample(n))
+    ensures 0 <= Model.Sample(n)(s).value < n
   {}
 
-  lemma IntervalSampleIsIndep(a: int, b: int)
+  lemma IntervalSampleBound(a: int, b: int, s: Rand.Bitstream)
     requires a < b
-    ensures Independence.IsIndep(Model.IntervalSample(a, b))
+    ensures a <= Model.IntervalSample(a, b)(s).value < b
   {
-    SampleIsIndep(b-a);
-    Independence.MapIsIndep(Model.Sample(b-a), x => a + x);
+    SampleBound(b-a, s);
+  }
+
+  lemma SampleIsMeasurePreserving(n: nat)
+    requires n > 0
+    ensures forall n | n > 0 :: Measures.IsMeasurePreserving(Rand.eventSpace, Rand.prob, Rand.eventSpace, Rand.prob, s => Model.Sample(n)(s).rest)
+  {}
+
+  lemma IntervalSampleIsMeasurePreserving(a: int, b: int)
+    requires a < b
+    ensures Measures.IsMeasurePreserving(Rand.eventSpace, Rand.prob, Rand.eventSpace, Rand.prob, s => Model.IntervalSample(a, b)(s).rest)
+  {
+    var f := s => Model.IntervalSample(a, b)(s).rest;
+    var f' := s => Model.Sample(b-a)(s).rest;
+
+    forall e: iset<Rand.Bitstream> | e in Rand.eventSpace ensures Measures.PreImage(f, e) == Measures.PreImage(f', e) {
+      forall s ensures s in Measures.PreImage(f, e) <==> s in Measures.PreImage(f', e) {
+        calc {
+          s in Measures.PreImage(f, e);
+          f(s) in e;
+          Model.IntervalSample(a, b)(s).rest in e;
+          Model.Sample(b-a)(s).rest in e;
+          f'(s) in e;
+          s in Measures.PreImage(f', e);
+        }
+      }
+    }
+
+    assert Measures.IsMeasurable(Rand.eventSpace, Rand.eventSpace, f) by {
+      forall e: iset<Rand.Bitstream> | e in Rand.eventSpace ensures Measures.PreImage(f, e) in Rand.eventSpace {
+        assert Measures.PreImage(f, e) == Measures.PreImage(f', e);
+        SampleIsMeasurePreserving(b-a);
+      }
+    }
+
+    forall e | e in Rand.eventSpace ensures Rand.prob(Measures.PreImage(f, e)) == Rand.prob(e) {
+      assert Measures.PreImage(f, e) == Measures.PreImage(f', e);
+      SampleIsMeasurePreserving(b-a);
+    }
+
   }
 }
diff --git a/src/Distributions/Uniform/Model.dfy b/src/Distributions/Uniform/Model.dfy
index d94a7fa9..1ae97e26 100644
--- a/src/Distributions/Uniform/Model.dfy
+++ b/src/Distributions/Uniform/Model.dfy
@@ -16,10 +16,15 @@ module Uniform.Model {
   ************/
 
   // Definition 49
-  opaque ghost function {:axiom} Sample(n: nat): (h: Monad.Hurd<nat>)
+  ghost function {:axiom} Sample(n: nat): (h: Monad.Hurd<nat>)
     requires n > 0
-    ensures Independence.IsIndep(h)
+    ensures Independence.IsIndepFunction(h)
+    ensures Measures.IsMeasurePreserving(Rand.eventSpace, Rand.prob, Rand.eventSpace, Rand.prob, s => h(s).rest)
     ensures forall s :: 0 <= h(s).value < n
+    ensures forall i | 0 <= i < n ::
+              var e := iset s | h(s).Equals(i);
+              && e in Rand.eventSpace
+              && Rand.prob(e) == 1.0 / (n as real)
 
   ghost function IntervalSample(a: int, b: int): (f: Monad.Hurd<int>)
     requires a < b
@@ -27,24 +32,4 @@ module Uniform.Model {
     Monad.Map(Sample(b - a), x => a + x)
   }
 
-  /*******
-   Lemmas
-  *******/
-
-  lemma SampleBound(n: nat, s: Rand.Bitstream)
-    requires n > 0
-    ensures 0 <= Sample(n)(s).value < n
-  {}
-
-  lemma IntervalSampleBound(a: int, b: int, s: Rand.Bitstream)
-    requires a < b
-    ensures a <= IntervalSample(a, b)(s).value < b
-  {
-    SampleBound(b-a, s);
-  }
-
-  lemma {:axiom} IntervalSampleIsMeasurePreserving(a: int, b: int)
-    requires a < b
-    ensures Measures.IsMeasurePreserving(Rand.eventSpace, Rand.prob, Rand.eventSpace, Rand.prob, s => IntervalSample(a, b)(s).rest)
-
 }
diff --git a/src/Math/RealArith.dfy b/src/Math/RealArith.dfy
index 402e0d9e..e8b0fa8c 100644
--- a/src/Math/RealArith.dfy
+++ b/src/Math/RealArith.dfy
@@ -178,4 +178,10 @@ module RealArith {
   lemma AsRealOfMultiplication(a: nat, b: nat)
     ensures (a as real) * (b as real) == (a * b) as real
   {}
+
+  lemma MultiplicationInvariance(a: real, b1: real, b2: real)
+    requires b1 == b2
+    ensures a * b1 == a * b2
+    ensures b1 * a == b2 * a
+  {}
 }
diff --git a/src/ProbabilisticProgramming/Independence.dfy b/src/ProbabilisticProgramming/Independence.dfy
index 694146c4..70eb61aa 100644
--- a/src/ProbabilisticProgramming/Independence.dfy
+++ b/src/ProbabilisticProgramming/Independence.dfy
@@ -26,9 +26,6 @@ module Independence {
     forall A: iset<A>, E: iset<Rand.Bitstream> | E in Rand.eventSpace :: IsIndepFunctionCondition(f, A, E)
   }
 
-  // Definition 35: (strong) independence
-  ghost predicate {:axiom} IsIndep<A(!new)>(f: Monad.Hurd<A>)
-
   /*******
    Lemmas
   *******/
@@ -66,15 +63,6 @@ module Independence {
     }
   }
 
-  // Equation (3.14)
-  lemma {:axiom} IsIndepImpliesIsIndepFunction<A(!new)>(f: Monad.Hurd<A>)
-    requires IsIndep(f)
-    ensures IsIndepFunction(f)
-
-  lemma {:axiom} MapIsIndep<A, B(!new)>(f: Monad.Hurd<A>, g: A -> B)
-    requires IsIndep(f)
-    ensures IsIndep(Monad.Map(f, g))
-
   lemma AreIndepEventsConjunctElimination(e1: iset<Rand.Bitstream>, e2: iset<Rand.Bitstream>)
     requires Measures.AreIndepEvents(Rand.eventSpace, Rand.prob, e1, e2)
     ensures Rand.prob(e1 * e2) == Rand.prob(e1) * Rand.prob(e2)
diff --git a/src/Util/FisherYates/Correctness.dfy b/src/Util/FisherYates/Correctness.dfy
index f54fdf35..266bb88c 100644
--- a/src/Util/FisherYates/Correctness.dfy
+++ b/src/Util/FisherYates/Correctness.dfy
@@ -136,27 +136,17 @@ module FisherYates.Correctness {
     }
   }
 
-  lemma CorrectnessFisherYatesUniqueElementsGeneralGreater1<T(!new)>(xs: seq<T>, p: seq<T>, i: nat)
-    decreases |xs| - i
+  lemma CorrectnessFisherYatesUniqueElementsGeneralGreater1ASingleton<T(!new)>(xs: seq<T>, p: seq<T>, i: nat) returns (j: nat)
     requires i <= |xs|
     requires i <= |p|
-    requires forall a, b | i <= a < b < |xs| :: xs[a] != xs[b]
     requires |xs| == |p|
+    requires forall a, b | i <= a < b < |xs| :: xs[a] != xs[b]
     requires multiset(p[i..]) == multiset(xs[i..])
     requires |xs[i..]| > 1
-    ensures CorrectnessPredicate(xs, p, i)
+    ensures
+      var A := iset j | i <= j < |xs| && xs[j] == p[i];
+      A != iset{} && A == iset{j}
   {
-    Model.PermutationsPreserveCardinality(p[i..], xs[i..]);
-    var e := iset s | Model.Shuffle(xs, i)(s).value[i..] == p[i..];
-    assert |xs| > i + 1;
-    var h := Uniform.Model.IntervalSample(i, |xs|);
-    assert hIsMeasurePreserving: Measures.IsMeasurePreserving(Rand.eventSpace, Rand.prob, Rand.eventSpace, Rand.prob, s => h(s).rest) by {
-      Uniform.Model.IntervalSampleIsMeasurePreserving(i, |xs|);
-    }
-    assert HIsIndependent: Independence.IsIndepFunction(h) by {
-      Uniform.Correctness.IntervalSampleIsIndep(i, |xs|);
-      Independence.IsIndepImpliesIsIndepFunction(h);
-    }
     var A := iset j | i <= j < |xs| && xs[j] == p[i];
     assert A != iset{} by {
       calc {
@@ -171,7 +161,7 @@ module FisherYates.Correctness {
         exists j :: j in A;
       }
     }
-    var j :| j in A;
+    j :| j in A;
     assert A == iset{j} by {
       assert forall k :: k in A <==> k in iset{j} by {
         forall k
@@ -193,12 +183,37 @@ module FisherYates.Correctness {
         }
       }
     }
-    assert BitStreamsInA: Monad.BitstreamsWithValueIn(h, A) == (iset s | Uniform.Model.IntervalSample(i, |xs|)(s).Equals(j)) by {
+  }
+
+  lemma CorrectnessFisherYatesUniqueElementsGeneralGreater1<T(!new)>(xs: seq<T>, p: seq<T>, i: nat)
+    decreases |xs| - i
+    requires i <= |xs|
+    requires i <= |p|
+    requires forall a, b | i <= a < b < |xs| :: xs[a] != xs[b]
+    requires |xs| == |p|
+    requires multiset(p[i..]) == multiset(xs[i..])
+    requires |xs[i..]| > 1
+    ensures CorrectnessPredicate(xs, p, i)
+  {
+    Model.PermutationsPreserveCardinality(p[i..], xs[i..]);
+    var e := CorrectnessConstructEvent(xs, p, i);
+    assert |xs| > i + 1;
+    var h := Uniform.Model.IntervalSample(i, |xs|);
+    assert Measures.IsMeasurePreserving(Rand.eventSpace, Rand.prob, Rand.eventSpace, Rand.prob, s => h(s).rest) by {
+      Uniform.Correctness.IntervalSampleIsMeasurePreserving(i, |xs|);
+    }
+    assert Independence.IsIndepFunction(h) by {
+      Uniform.Correctness.IntervalSampleIsIndepFunction(i, |xs|);
+    }
+    var A := iset j | i <= j < |xs| && xs[j] == p[i];
+    var j := CorrectnessFisherYatesUniqueElementsGeneralGreater1ASingleton(xs, p, i);
+    assert A == iset{j};
+    assert Monad.BitstreamsWithValueIn(h, A) == (iset s | Uniform.Model.IntervalSample(i, |xs|)(s).Equals(j)) by {
       BitStreamsInA(xs, p, i, j, h, A);
     }
     var ys := Model.Swap(xs, i, j);
     var e' := CorrectnessConstructEvent(ys, p, i+1);
-    assert InductionHypothesis: CorrectnessPredicate(ys, p, i+1) by {
+    assert CorrectnessPredicate(ys, p, i+1) by {
       assert multiset(ys[i+1..]) == multiset(p[i+1..]) by {
         InductionHypothesisPrecondition1(xs, ys, p, i, j);
       }
@@ -238,19 +253,13 @@ module FisherYates.Correctness {
         CorrectnessFisherYatesUniqueElementsGeneralLeq1(ys, p, i+1);
       }
     }
-    assert DecomposeE: e == Monad.BitstreamsWithValueIn(h, A) * Monad.BitstreamsWithRestIn(h, e') by {
+    assert e == Monad.BitstreamsWithValueIn(h, A) * Monad.BitstreamsWithRestIn(h, e') by {
       DecomposeE(xs, ys, p, i, j, h, A, e, e');
     }
 
     assert CorrectnessPredicate(xs, p, i) by {
-      reveal DecomposeE;
-      reveal HIsIndependent;
-      reveal BitStreamsInA;
-      reveal InductionHypothesis;
-      reveal hIsMeasurePreserving;
       CorrectnessFisherYatesUniqueElementsGeneralGreater1Helper(xs, ys, p, i, j, h, A, e, e');
     }
-
   }
 
   lemma CorrectnessFisherYatesUniqueElementsGeneralGreater1Helper<T(!new)>(xs: seq<T>, ys: seq<T>, p: seq<T>, i: nat, j: nat, h: Monad.Hurd<int>, A: iset<int>, e: iset<Rand.Bitstream>, e': iset<Rand.Bitstream>)
@@ -328,6 +337,111 @@ module FisherYates.Correctness {
     }
   }
 
+  lemma DecomposeEImplicationOne<T(!new)>(xs: seq<T>, ys: seq<T>, p: seq<T>, i: nat, j: nat, h: Monad.Hurd<int>, A: iset<int>, e: iset<Rand.Bitstream>, e': iset<Rand.Bitstream>, s: Rand.Bitstream)
+    requires i <= |p|
+    requires |xs| == |p|
+    requires |xs|-i > 1
+    requires i <= |xs|
+    requires forall a, b | i <= a < b < |xs| :: xs[a] != xs[b]
+    requires multiset(p[i..]) == multiset(xs[i..])
+    requires i <= j < |xs| && xs[j] == p[i]
+    requires A == iset j | i <= j < |xs| && xs[j] == p[i]
+    requires A == iset{j}
+    requires h == Uniform.Model.IntervalSample(i, |xs|)
+    requires ys == Model.Swap(xs, i, j)
+    requires e == CorrectnessConstructEvent(xs, p, i)
+    requires e' == CorrectnessConstructEvent(ys, p, i+1)
+    requires s in e
+    ensures s in Monad.BitstreamsWithValueIn(h, A) * Monad.BitstreamsWithRestIn(h, e')
+  {
+    assert s in Monad.BitstreamsWithValueIn(h, A) * Monad.BitstreamsWithRestIn(h, e') by {
+      var zs := Model.Shuffle(xs, i)(s).value;
+      assert zs[i..] == p[i..];
+      var k := Uniform.Model.IntervalSample(i, |xs|)(s).value;
+      Uniform.Correctness.IntervalSampleBound(i, |xs|, s);
+      var s' := Uniform.Model.IntervalSample(i, |xs|)(s).rest;
+
+      assert s in Monad.BitstreamsWithValueIn(h, A) by {
+        var ys' := Model.Swap(xs, i, k);
+        var zs' := Model.Shuffle(ys', i+1)(s').value;
+        assert zs == zs';
+        calc {
+          p[i];
+          zs[i];
+          zs'[i];
+          { assert Model.ShuffleInvariancePredicatePointwise(ys', Model.Shuffle(ys', i+1)(s'), i); }
+          ys'[i];
+          xs[k];
+        }
+        assert k in A;
+      }
+
+      assert s in Monad.BitstreamsWithRestIn(h, e') by {
+        assert Model.Shuffle(ys, i+1)(s').value[i+1..] == p[i+1..] by {
+          forall j | 0 <= j < |xs| - (i+1) ensures Model.Shuffle(ys, i+1)(s').value[i+1..][j] == p[i+1..][j] {
+            calc {
+              Model.Shuffle(ys, i+1)(s').value[i+1..][j];
+              Model.ShuffleCurried(ys, s', i+1).value[i+1..][j];
+              Model.ShuffleCurried(xs, s, i).value[i+1..][j];
+              Model.Shuffle(xs, i)(s).value[i+1..][j];
+              Model.Shuffle(xs, i)(s).value[i..][j+1];
+              { assert Model.Shuffle(xs, i)(s).value[i..] == p[i..]; }
+              p[i..][j+1];
+              p[i+1..][j];
+            }
+          }
+        }
+      }
+    }
+  }
+
+  lemma DecomposeEImplicationTwo<T(!new)>(xs: seq<T>, ys: seq<T>, p: seq<T>, i: nat, j: nat, h: Monad.Hurd<int>, A: iset<int>, e: iset<Rand.Bitstream>, e': iset<Rand.Bitstream>, s: Rand.Bitstream)
+    requires i <= |p|
+    requires |xs| == |p|
+    requires |xs|-i > 1
+    requires i <= |xs|
+    requires forall a, b | i <= a < b < |xs| :: xs[a] != xs[b]
+    requires multiset(p[i..]) == multiset(xs[i..])
+    requires i <= j < |xs| && xs[j] == p[i]
+    requires A == iset j | i <= j < |xs| && xs[j] == p[i]
+    requires A == iset{j}
+    requires h == Uniform.Model.IntervalSample(i, |xs|)
+    requires ys == Model.Swap(xs, i, j)
+    requires e == CorrectnessConstructEvent(xs, p, i)
+    requires e' == CorrectnessConstructEvent(ys, p, i+1)
+    requires s in Monad.BitstreamsWithValueIn(h, A) * Monad.BitstreamsWithRestIn(h, e')
+    ensures s in e
+  {
+    var k := Uniform.Model.IntervalSample(i, |xs|)(s).value;
+    assert k in A;
+    assert k == j;
+    var s' := Uniform.Model.IntervalSample(i, |xs|)(s).rest;
+    assert s' in e';
+    var ys' := Model.Swap(xs, i, k);
+    assert ys' == ys;
+    var zs' := Model.Shuffle(ys', i+1)(s').value;
+    assert Model.Shuffle(xs, i)(s).value[i..] == p[i..] by {
+      calc {
+        Model.Shuffle(xs, i)(s).value[i..];
+        { assert Model.Shuffle(xs, i)(s).value == zs'; }
+        zs'[i..];
+        Model.Shuffle(ys', i+1)(s').value[i..];
+        { assert ys' == ys; }
+        Model.Shuffle(ys, i+1)(s').value[i..];
+        { SliceOfSequences(Model.Shuffle(ys, i+1)(s').value, i); }
+        [Model.Shuffle(ys, i+1)(s').value[i]] + Model.Shuffle(ys, i+1)(s').value[i+1..];
+        { assert Model.ShuffleInvariancePredicatePointwise(ys, Model.Shuffle(ys, i+1)(s'), i); assert Model.Shuffle(ys, i+1)(s').value[i] == ys[i]; }
+        [ys[i]] + Model.Shuffle(ys, i+1)(s').value[i+1..];
+        { assert ys[i] == xs[k]; }
+        [xs[k]] + Model.Shuffle(ys, i+1)(s').value[i+1..];
+        { assert xs[k] == p[i]; }
+        [p[i]] + p[i+1..];
+        { SliceOfSequences(p, i); }
+        p[i..];
+      }
+    }
+  }
+
   lemma DecomposeE<T(!new)>(xs: seq<T>, ys: seq<T>, p: seq<T>, i: nat, j: nat, h: Monad.Hurd<int>, A: iset<int>, e: iset<Rand.Bitstream>, e': iset<Rand.Bitstream>)
     requires i <= |p|
     requires |xs| == |p|
@@ -340,71 +454,19 @@ module FisherYates.Correctness {
     requires A == iset{j}
     requires h == Uniform.Model.IntervalSample(i, |xs|)
     requires ys == Model.Swap(xs, i, j)
-    requires e == iset s | Model.Shuffle(xs, i)(s).value[i..] == p[i..]
-    requires e' == iset s | Model.Shuffle(ys, i+1)(s).value[i+1..] == p[i+1..]
+    requires e == CorrectnessConstructEvent(xs, p, i)
+    requires e' == CorrectnessConstructEvent(ys, p, i+1)
     ensures e == Monad.BitstreamsWithValueIn(h, A) * Monad.BitstreamsWithRestIn(h, e')
   {
-    assert forall s :: s in e <==> s in Monad.BitstreamsWithValueIn(h, A) * Monad.BitstreamsWithRestIn(h, e') by {
+    assert e == Monad.BitstreamsWithValueIn(h, A) * Monad.BitstreamsWithRestIn(h, e') by {
       forall s
         ensures s in e <==> s in Monad.BitstreamsWithValueIn(h, A) * Monad.BitstreamsWithRestIn(h, e')
       {
         if s in e {
-          var zs := Model.Shuffle(xs, i)(s).value;
-          assert zs[i..] == p[i..];
-          var k := Uniform.Model.IntervalSample(i, |xs|)(s).value;
-          Uniform.Model.IntervalSampleBound(i, |xs|, s);
-          var s' := Uniform.Model.IntervalSample(i, |xs|)(s).rest;
-          assert s in Monad.BitstreamsWithValueIn(h, A) by {
-            var ys' := Model.Swap(xs, i, k);
-            var zs' := Model.Shuffle(ys', i+1)(s').value;
-            assert zs == zs';
-            calc {
-              p[i];
-              zs[i];
-              zs'[i];
-              { assert Model.ShuffleInvariancePredicatePointwise(ys', Model.Shuffle(ys', i+1)(s'), i); }
-              ys'[i];
-              xs[k];
-            }
-            assert k in A;
-          }
-          assert s in Monad.BitstreamsWithRestIn(h, e') by {
-            assert Model.Shuffle(ys, i+1)(s').value[i+1..] == p[i+1..];
-          }
-          assert s in Monad.BitstreamsWithValueIn(h, A) * Monad.BitstreamsWithRestIn(h, e');
+          DecomposeEImplicationOne(xs, ys, p, i, j, h, A, e, e', s);
         }
-
         if s in Monad.BitstreamsWithValueIn(h, A) * Monad.BitstreamsWithRestIn(h, e') {
-          assert s in e by {
-            var k := Uniform.Model.IntervalSample(i, |xs|)(s).value;
-            assert k in A;
-            assert k == j;
-            var s' := Uniform.Model.IntervalSample(i, |xs|)(s).rest;
-            assert s' in e';
-            var ys' := Model.Swap(xs, i, k);
-            assert ys' == ys;
-            var zs' := Model.Shuffle(ys', i+1)(s').value;
-            assert Model.Shuffle(xs, i)(s).value[i..] == p[i..] by {
-              calc {
-                Model.Shuffle(xs, i)(s).value[i..];
-                { assert Model.Shuffle(xs, i)(s).value == zs'; }
-                zs'[i..];
-                Model.Shuffle(ys', i+1)(s').value[i..];
-                { assert ys' == ys; }
-                Model.Shuffle(ys, i+1)(s').value[i..];
-                { SliceOfSequences(Model.Shuffle(ys, i+1)(s').value, i); }
-                [Model.Shuffle(ys, i+1)(s').value[i]] + Model.Shuffle(ys, i+1)(s').value[i+1..];
-                { assert Model.ShuffleInvariancePredicatePointwise(ys, Model.Shuffle(ys, i+1)(s'), i); assert Model.Shuffle(ys, i+1)(s').value[i] == ys[i]; }
-                [ys[i]] + Model.Shuffle(ys, i+1)(s').value[i+1..];
-                { assert ys[i] == xs[k]; }
-                [xs[k]] + Model.Shuffle(ys, i+1)(s').value[i+1..];
-                { assert xs[k] == p[i]; }
-                [p[i]] + p[i+1..];
-                { SliceOfSequences(p, i); }
-                p[i..];
-              }
-            }
-          }
+          DecomposeEImplicationTwo(xs, ys, p, i, j, h, A, e, e', s);
         }
       }
     }
@@ -514,7 +576,7 @@ module FisherYates.Correctness {
     reveal DecomposeE;
   }
 
-  lemma ProbabilityOfE<T(!new)>(xs: seq<T>, ys: seq<T>, p: seq<T>, i: nat, j: nat, h: Monad.Hurd<int>, A: iset<int>, e: iset<Rand.Bitstream>, e': iset<Rand.Bitstream>)
+  lemma {:vcs_split_on_every_assert} ProbabilityOfE<T(!new)>(xs: seq<T>, ys: seq<T>, p: seq<T>, i: nat, j: nat, h: Monad.Hurd<int>, A: iset<int>, e: iset<Rand.Bitstream>, e': iset<Rand.Bitstream>)
     requires i <= |xs|
     requires i <= |p|
     requires forall a, b | i <= a < b < |xs| :: xs[a] != xs[b]
@@ -533,25 +595,76 @@ module FisherYates.Correctness {
     ensures
       Rand.prob(e) == 1.0 / (NatArith.FactorialTraditional(|xs|-i) as real)
   {
+    var e'' := iset s | Uniform.Model.IntervalSample(i, |xs|)(s).Equals(j);
+    assert BitStreamsInALifted: Rand.prob(Monad.BitstreamsWithValueIn(h, A)) * Rand.prob(e') == Rand.prob(e'') * Rand.prob(e') by {
+      assert Rand.prob(Monad.BitstreamsWithValueIn(h, A)) == Rand.prob(e'') by {
+        reveal BitStreamsInA;
+      }
+    }
+
+    assert FullIntervalLifted: Rand.prob(e'') * Rand.prob(e') == (1.0 / ((|xs|-i) as real)) * Rand.prob(e') by {
+      assert Rand.prob(e'') == 1.0 / ((|xs|-i) as real) by {
+        Uniform.Correctness.UniformFullIntervalCorrectness(i, |xs|, j);
+      }
+      RealArith.MultiplicationInvariance(Rand.prob(e'), Rand.prob(e''), 1.0 / ((|xs|-i) as real));
+    }
+
+    var denom := NatArith.FactorialTraditional(|xs|-(i+1)) as real;
+    var denom2 := NatArith.FactorialTraditional((|xs|-i)-1) as real;
+    var frac := 1.0 / denom;
+    var frac2 := 1.0 / denom2;
+
+    assert InductionHypothesisLifted: (1.0 / ((|xs|-i) as real)) * Rand.prob(e') == (1.0 / ((|xs|-i) as real)) * frac by {
+      assert Rand.prob(e') == frac by {
+        reveal InductionHypothesis;
+      }
+      RealArith.MultiplicationInvariance(1.0 / ((|xs|-i) as real), Rand.prob(e'), frac);
+    }
+
+    assert FracLifted: (1.0 / ((|xs|-i) as real)) * frac == (1.0 / ((|xs|-i) as real)) * frac2 by {
+      assert frac == frac2;
+      RealArith.MultiplicationInvariance(1.0 / ((|xs|-i) as real), frac, frac2);
+    }
+
+    assert SimplifyFractionsMultiplicationLifted: (1.0 / ((|xs|-i) as real)) * frac2 == (1.0 * 1.0) / (((|xs|-i) as real) * denom) by {
+      assert |xs|-i > 1;
+      RealArith.SimplifyFractionsMultiplication(1.0, (|xs|-i) as real, 1.0, denom);
+    }
+
+    assert AsRealOfMultiplicationLifted: 1.0 / (((|xs|-i) as real) * denom) == 1.0 / (((|xs|-i) * NatArith.FactorialTraditional((|xs|-i)-1)) as real) by {
+      assert ((|xs|-i) as real) * denom == ((|xs|-i) * NatArith.FactorialTraditional((|xs|-i)-1)) as real by {
+        RealArith.AsRealOfMultiplication(|xs|-i, NatArith.FactorialTraditional((|xs|-i)-1));
+      }
+    }
+
+    assert NonZero: (((|xs|-i) * NatArith.FactorialTraditional((|xs|-i)-1)) as real) != 0.0 by {
+      assert |xs|-i != 0;
+      assert NatArith.FactorialTraditional((|xs|-i)-1) != 0;
+    }
+
+    assert NonZeroDenom: denom != 0.0 by {
+      assert NatArith.FactorialTraditional((|xs|-i)-1) != 0;
+    }
+
     calc {
       Rand.prob(e);
       { reveal DecomposeE; }
       Rand.prob(Monad.BitstreamsWithValueIn(h, A) * Monad.BitstreamsWithRestIn(h, e'));
       { reveal HIsIndependent; reveal InductionHypothesis; reveal hIsMeasurePreserving; Independence.ResultsIndependent(h, A, e'); }
       Rand.prob(Monad.BitstreamsWithValueIn(h, A)) * Rand.prob(e');
-      { assert Rand.prob(Monad.BitstreamsWithValueIn(h, A)) == Rand.prob(iset s | Uniform.Model.IntervalSample(i, |xs|)(s).Equals(j)) by { reveal BitStreamsInA; } }
-      Rand.prob(iset s | Uniform.Model.IntervalSample(i, |xs|)(s).Equals(j)) * Rand.prob(e');
-      { assert Rand.prob(iset s | Uniform.Model.IntervalSample(i, |xs|)(s).Equals(j)) ==  (1.0 / ((|xs|-i) as real)) by { Uniform.Correctness.UniformFullIntervalCorrectness(i, |xs|, j); } }
+      { reveal BitStreamsInALifted; }
+      Rand.prob(e'') * Rand.prob(e');
+      { reveal FullIntervalLifted; }
       (1.0 / ((|xs|-i) as real)) * Rand.prob(e');
-      { assert Rand.prob(e') == (1.0 / (NatArith.FactorialTraditional(|xs|-(i+1)) as real)) by { reveal InductionHypothesis; } }
-      (1.0 / ((|xs|-i) as real)) * (1.0 / (NatArith.FactorialTraditional(|xs|-(i+1)) as real));
-      { assert (NatArith.FactorialTraditional(|xs|-(i+1)) as real) == (NatArith.FactorialTraditional((|xs|-i)-1) as real) by { assert |xs|-(i+1) == (|xs|-i)-1; } }
-      (1.0 / ((|xs|-i) as real)) * (1.0 / (NatArith.FactorialTraditional((|xs|-i)-1) as real));
-      { assert |xs|-i > 1; RealArith.SimplifyFractionsMultiplication(1.0, (|xs|-i) as real, 1.0, NatArith.FactorialTraditional((|xs|-i)-1) as real); }
-      (1.0 * 1.0) / (((|xs|-i) as real) * (NatArith.FactorialTraditional((|xs|-i)-1) as real));
+      { reveal InductionHypothesisLifted; }
+      (1.0 / ((|xs|-i) as real)) * frac;
+      { reveal FracLifted; }
+      (1.0 / ((|xs|-i) as real)) * frac2;
+      { reveal SimplifyFractionsMultiplicationLifted; reveal NonZeroDenom; }
+      (1.0 * 1.0) / (((|xs|-i) as real) * denom);
       { assert 1.0 * 1.0 == 1.0; }
-      1.0 / (((|xs|-i) as real) * (NatArith.FactorialTraditional((|xs|-i)-1) as real));
-      { RealArith.AsRealOfMultiplication(|xs|-i, NatArith.FactorialTraditional((|xs|-i)-1)); }
+      1.0 / (((|xs|-i) as real) * denom);
+      { reveal AsRealOfMultiplicationLifted; reveal NonZero; }
       1.0 / (((|xs|-i) * NatArith.FactorialTraditional((|xs|-i)-1)) as real);
       { assert (|xs|-i) * NatArith.FactorialTraditional((|xs|-i)-1) == NatArith.FactorialTraditional(|xs|-i) by { reveal NatArith.FactorialTraditional(); } }
       1.0 / (NatArith.FactorialTraditional(|xs|-i) as real);
diff --git a/src/Util/FisherYates/Equivalence.dfy b/src/Util/FisherYates/Equivalence.dfy
index cf20a1cd..98fbf7ba 100644
--- a/src/Util/FisherYates/Equivalence.dfy
+++ b/src/Util/FisherYates/Equivalence.dfy
@@ -6,6 +6,7 @@
 module FisherYates.Equivalence {
   import Model
   import Rand
+  import Monad
 
   ghost predicate LoopInvariant<T>(prevI: nat, i: nat, a: array<T>, prevASeq: seq<T>, oldASeq: seq<T>, oldS: Rand.Bitstream, prevS: Rand.Bitstream, s: Rand.Bitstream)
     reads a
@@ -16,4 +17,20 @@ module FisherYates.Equivalence {
     && Model.Shuffle(prevASeq, prevI)(prevS) == Model.Shuffle(a[..], i)(s)
   }
 
+  lemma ShuffleElseClause<T>(a: array<T>, oldASeq: seq<T>, oldS: Rand.Bitstream, s: Rand.Bitstream)
+    requires aLength: a.Length <= 1
+    requires aInvariant: oldASeq == a[..]
+    requires sInvariant: oldS == s
+    ensures Model.Shuffle(oldASeq)(oldS) == Monad.Result(a[..], s)
+  {
+    calc {
+      Model.Shuffle(oldASeq)(oldS);
+      { reveal aInvariant; reveal sInvariant; }
+      Model.Shuffle(a[..])(s);
+      Model.ShuffleCurried(a[..], s);
+      { reveal aLength; assert |a[..]| == a.Length; }
+      Monad.Return(a[..])(s);
+      Monad.Result(a[..], s);
+    }
+  }
 }
\ No newline at end of file
diff --git a/src/Util/FisherYates/Implementation.dfy b/src/Util/FisherYates/Implementation.dfy
index 0510c446..d0f4f63d 100644
--- a/src/Util/FisherYates/Implementation.dfy
+++ b/src/Util/FisherYates/Implementation.dfy
@@ -20,7 +20,7 @@ module FisherYates.Implementation {
       ghost var prevI, prevASeq, prevS := 0, a[..], s; // ghost
       if a.Length > 1 {
         for i := 0 to a.Length - 1
-          invariant Equivalence.LoopInvariant(prevI, i, a, prevASeq, old(a[..]), old(s), prevS, s)
+          invariant Equivalence.LoopInvariant(prevI, i, a, prevASeq, old(a[..]), old(s), prevS, s) // ghost
         {
           prevI, prevASeq, prevS := i, a[..], s; // ghost
           var j := UniformIntervalSample(i, a.Length);
@@ -28,7 +28,7 @@ module FisherYates.Implementation {
           Swap(a, i, j);
         }
       } else {
-        assert prevASeq == a[..]; // ghost
+        Equivalence.ShuffleElseClause(a, old(a[..]), old(s), s); // ghost
       }
 
     }
diff --git a/src/Util/FisherYates/Model.dfy b/src/Util/FisherYates/Model.dfy
index 5d45a141..91fc970e 100644
--- a/src/Util/FisherYates/Model.dfy
+++ b/src/Util/FisherYates/Model.dfy
@@ -13,9 +13,10 @@ module FisherYates.Model {
   ************/
 
   ghost predicate ShuffleInvariancePredicatePointwise<T>(xs: seq<T>, r: Monad.Result<seq<T>>, j: int)
+    requires |r.value| == |xs|
     requires 0 <= j < |xs|
   {
-    |r.value| == |xs| && r.value[j] == xs[j]
+    r.value[j] == xs[j]
   }
 
   ghost function Shuffle<T>(xs: seq<T>, i: nat := 0): (h: Monad.Hurd<seq<T>>)
@@ -34,7 +35,7 @@ module FisherYates.Model {
   {
     if |xs| - i > 1 then
       var (j, s') := Uniform.Model.IntervalSample(i, |xs|)(s).Extract();
-      assert i <= j < |xs| by { Uniform.Model.IntervalSampleBound(i, |xs|, s); }
+      assert i <= j < |xs| by { Uniform.Correctness.IntervalSampleBound(i, |xs|, s); }
       var ys := Swap(xs, i, j);
       var r := ShuffleCurried(ys, s', i + 1);
       assert forall j | 0 <= j < i :: ShuffleInvariancePredicatePointwise(xs, r, j) by {