diff --git a/src/Distributions/Base/Interface.dfy b/src/Distributions/Base/Interface.dfy
index 72766ddf..19a478bf 100644
--- a/src/Distributions/Base/Interface.dfy
+++ b/src/Distributions/Base/Interface.dfy
@@ -1,7 +1,7 @@
 /*******************************************************************************
-*  Copyright by the contributors to the Dafny Project
-*  SPDX-License-Identifier: MIT
-*******************************************************************************/
+ *  Copyright by the contributors to the Dafny Project
+ *  SPDX-License-Identifier: MIT
+ *******************************************************************************/
 
 include "../../ProbabilisticProgramming/RandomNumberGenerator.dfy"
 include "Model.dfy"
diff --git a/src/Distributions/Base/Model.dfy b/src/Distributions/Base/Model.dfy
index 3ebd0ec9..0c833f30 100644
--- a/src/Distributions/Base/Model.dfy
+++ b/src/Distributions/Base/Model.dfy
@@ -1,7 +1,7 @@
 /*******************************************************************************
-*  Copyright by the contributors to the Dafny Project
-*  SPDX-License-Identifier: MIT
-*******************************************************************************/
+ *  Copyright by the contributors to the Dafny Project
+ *  SPDX-License-Identifier: MIT
+ *******************************************************************************/
 
 include "../../ProbabilisticProgramming/RandomNumberGenerator.dfy"
 include "../../ProbabilisticProgramming/Monad.dfy"
diff --git a/src/Distributions/Bernoulli/Correctness.dfy b/src/Distributions/Bernoulli/Correctness.dfy
index 981bd332..3ad807d7 100644
--- a/src/Distributions/Bernoulli/Correctness.dfy
+++ b/src/Distributions/Bernoulli/Correctness.dfy
@@ -1,7 +1,7 @@
 /*******************************************************************************
-*  Copyright by the contributors to the Dafny Project
-*  SPDX-License-Identifier: MIT
-*******************************************************************************/
+ *  Copyright by the contributors to the Dafny Project
+ *  SPDX-License-Identifier: MIT
+ *******************************************************************************/
 
 include "../../Math/MeasureTheory.dfy"
 include "../../ProbabilisticProgramming/RandomNumberGenerator.dfy"
@@ -13,7 +13,7 @@ module BernoulliCorrectness {
   import RandomNumberGenerator
   import Independence
   import BernoulliModel
-  
+
   /*******
    Lemmas
   *******/
diff --git a/src/Distributions/Bernoulli/Implementation.dfy b/src/Distributions/Bernoulli/Implementation.dfy
index 5a797227..45620781 100644
--- a/src/Distributions/Bernoulli/Implementation.dfy
+++ b/src/Distributions/Bernoulli/Implementation.dfy
@@ -1,7 +1,7 @@
 /*******************************************************************************
-*  Copyright by the contributors to the Dafny Project
-*  SPDX-License-Identifier: MIT
-*******************************************************************************/
+ *  Copyright by the contributors to the Dafny Project
+ *  SPDX-License-Identifier: MIT
+ *******************************************************************************/
 
 include "../../Math/MeasureTheory.dfy"
 include "Interface.dfy"
diff --git a/src/Distributions/Bernoulli/Interface.dfy b/src/Distributions/Bernoulli/Interface.dfy
index f714fb1a..27a5d07b 100644
--- a/src/Distributions/Bernoulli/Interface.dfy
+++ b/src/Distributions/Bernoulli/Interface.dfy
@@ -1,7 +1,7 @@
 /*******************************************************************************
-*  Copyright by the contributors to the Dafny Project
-*  SPDX-License-Identifier: MIT
-*******************************************************************************/
+ *  Copyright by the contributors to the Dafny Project
+ *  SPDX-License-Identifier: MIT
+ *******************************************************************************/
 
 include "../Base/Interface.dfy"
 include "Model.dfy"
diff --git a/src/Distributions/Bernoulli/Model.dfy b/src/Distributions/Bernoulli/Model.dfy
index 6844e881..c93cd412 100644
--- a/src/Distributions/Bernoulli/Model.dfy
+++ b/src/Distributions/Bernoulli/Model.dfy
@@ -1,7 +1,7 @@
 /*******************************************************************************
-*  Copyright by the contributors to the Dafny Project
-*  SPDX-License-Identifier: MIT
-*******************************************************************************/
+ *  Copyright by the contributors to the Dafny Project
+ *  SPDX-License-Identifier: MIT
+ *******************************************************************************/
 
 include "../../Math/MeasureTheory.dfy"
 include "../../ProbabilisticProgramming/Monad.dfy"
@@ -16,15 +16,9 @@ module BernoulliModel {
     var f :=
       (b: bool) =>
         if b then
-          if p <= 0.5 then
-            Monad.Return(false)
-          else
-            ProbBernoulli(2.0 * p - 1.0)
+          (if p <= 0.5 then Monad.Return(false) else ProbBernoulli(2.0 * p - 1.0))
         else
-          if p <= 0.5 then
-            ProbBernoulli(2.0 * p)
-          else
-            Monad.Return(true);
+          (if p <= 0.5 then ProbBernoulli(2.0 * p) else Monad.Return(true));
     Monad.Bind(Monad.Deconstruct, f)
   }
 }
diff --git a/src/Distributions/BernoulliExpNeg/Implementation.dfy b/src/Distributions/BernoulliExpNeg/Implementation.dfy
index 89d7291b..660c3efe 100644
--- a/src/Distributions/BernoulliExpNeg/Implementation.dfy
+++ b/src/Distributions/BernoulliExpNeg/Implementation.dfy
@@ -1,7 +1,7 @@
 /*******************************************************************************
-*  Copyright by the contributors to the Dafny Project
-*  SPDX-License-Identifier: MIT
-*******************************************************************************/
+ *  Copyright by the contributors to the Dafny Project
+ *  SPDX-License-Identifier: MIT
+ *******************************************************************************/
 
 include "../Bernoulli/Interface.dfy"
 include "Interface.dfy"
diff --git a/src/Distributions/BernoulliExpNeg/Interface.dfy b/src/Distributions/BernoulliExpNeg/Interface.dfy
index e41624e1..f78cf989 100644
--- a/src/Distributions/BernoulliExpNeg/Interface.dfy
+++ b/src/Distributions/BernoulliExpNeg/Interface.dfy
@@ -1,13 +1,13 @@
 /*******************************************************************************
-*  Copyright by the contributors to the Dafny Project
-*  SPDX-License-Identifier: MIT
-*******************************************************************************/
+ *  Copyright by the contributors to the Dafny Project
+ *  SPDX-License-Identifier: MIT
+ *******************************************************************************/
 
 include "../Bernoulli/Interface.dfy"
 
 module BernoulliExpNegInterface {
   import BernoulliInterface
-  
+
   trait {:termination false} IBernoulliExpNeg extends BernoulliInterface.IBernoulli {
 
     method BernoulliExpNeg(gamma: real) returns (c: bool)
diff --git a/src/Distributions/BernoulliRational/Correctness.dfy b/src/Distributions/BernoulliRational/Correctness.dfy
index 81bfd883..9bfda219 100644
--- a/src/Distributions/BernoulliRational/Correctness.dfy
+++ b/src/Distributions/BernoulliRational/Correctness.dfy
@@ -1,7 +1,7 @@
 /*******************************************************************************
-*  Copyright by the contributors to the Dafny Project
-*  SPDX-License-Identifier: MIT
-*******************************************************************************/
+ *  Copyright by the contributors to the Dafny Project
+ *  SPDX-License-Identifier: MIT
+ *******************************************************************************/
 
 include "../../Math/MeasureTheory.dfy"
 include "../../Math/Helper.dfy"
diff --git a/src/Distributions/BernoulliRational/Implementation.dfy b/src/Distributions/BernoulliRational/Implementation.dfy
index ba672828..b9d9655a 100644
--- a/src/Distributions/BernoulliRational/Implementation.dfy
+++ b/src/Distributions/BernoulliRational/Implementation.dfy
@@ -1,7 +1,7 @@
 /*******************************************************************************
-*  Copyright by the contributors to the Dafny Project
-*  SPDX-License-Identifier: MIT
-*******************************************************************************/
+ *  Copyright by the contributors to the Dafny Project
+ *  SPDX-License-Identifier: MIT
+ *******************************************************************************/
 
 include "Interface.dfy"
 include "Model.dfy"
@@ -12,7 +12,7 @@ module BernoulliRationalImplementation {
 
   trait {:termination false} TBernoulliRational extends BernoulliRationalInterface.IBernoulliRational {
 
-   method BernoulliRational(m: nat, n: nat) returns (c: bool)
+    method BernoulliRational(m: nat, n: nat) returns (c: bool)
       modifies this
       decreases *
       requires n != 0
diff --git a/src/Distributions/BernoulliRational/Interface.dfy b/src/Distributions/BernoulliRational/Interface.dfy
index 8f9c4010..f883bf51 100644
--- a/src/Distributions/BernoulliRational/Interface.dfy
+++ b/src/Distributions/BernoulliRational/Interface.dfy
@@ -1,7 +1,7 @@
 /*******************************************************************************
-*  Copyright by the contributors to the Dafny Project
-*  SPDX-License-Identifier: MIT
-*******************************************************************************/
+ *  Copyright by the contributors to the Dafny Project
+ *  SPDX-License-Identifier: MIT
+ *******************************************************************************/
 
 include "../Uniform/Interface.dfy"
 include "Model.dfy"
@@ -9,7 +9,7 @@ include "Model.dfy"
 module BernoulliRationalInterface {
   import UniformInterface
   import BernoulliRationalModel
-  
+
   trait {:termination false} IBernoulliRational extends UniformInterface.IUniform {
 
     method BernoulliRational(m: nat, n: nat) returns (c: bool)
diff --git a/src/Distributions/BernoulliRational/Model.dfy b/src/Distributions/BernoulliRational/Model.dfy
index 734254db..617fe913 100644
--- a/src/Distributions/BernoulliRational/Model.dfy
+++ b/src/Distributions/BernoulliRational/Model.dfy
@@ -1,7 +1,7 @@
 /*******************************************************************************
-*  Copyright by the contributors to the Dafny Project
-*  SPDX-License-Identifier: MIT
-*******************************************************************************/
+ *  Copyright by the contributors to the Dafny Project
+ *  SPDX-License-Identifier: MIT
+ *******************************************************************************/
 
 include "../Uniform/Model.dfy"
 include "../../ProbabilisticProgramming/Monad.dfy"
diff --git a/src/Distributions/DiscreteGaussian/Implementation.dfy b/src/Distributions/DiscreteGaussian/Implementation.dfy
index 5819f861..66cc2e07 100644
--- a/src/Distributions/DiscreteGaussian/Implementation.dfy
+++ b/src/Distributions/DiscreteGaussian/Implementation.dfy
@@ -1,7 +1,7 @@
 /*******************************************************************************
-*  Copyright by the contributors to the Dafny Project
-*  SPDX-License-Identifier: MIT
-*******************************************************************************/
+ *  Copyright by the contributors to the Dafny Project
+ *  SPDX-License-Identifier: MIT
+ *******************************************************************************/
 
 include "Interface.dfy"
 
diff --git a/src/Distributions/DiscreteGaussian/Interface.dfy b/src/Distributions/DiscreteGaussian/Interface.dfy
index a162ad6a..5f036d2f 100644
--- a/src/Distributions/DiscreteGaussian/Interface.dfy
+++ b/src/Distributions/DiscreteGaussian/Interface.dfy
@@ -1,7 +1,7 @@
 /*******************************************************************************
-*  Copyright by the contributors to the Dafny Project
-*  SPDX-License-Identifier: MIT
-*******************************************************************************/
+ *  Copyright by the contributors to the Dafny Project
+ *  SPDX-License-Identifier: MIT
+ *******************************************************************************/
 
 include "../BernoulliExpNeg/Interface.dfy"
 include "../DiscreteLaplace/Interface.dfy"
diff --git a/src/Distributions/DiscreteLaplace/Implementation.dfy b/src/Distributions/DiscreteLaplace/Implementation.dfy
index 42c5f036..e5fb839e 100644
--- a/src/Distributions/DiscreteLaplace/Implementation.dfy
+++ b/src/Distributions/DiscreteLaplace/Implementation.dfy
@@ -1,7 +1,7 @@
 /*******************************************************************************
-*  Copyright by the contributors to the Dafny Project
-*  SPDX-License-Identifier: MIT
-*******************************************************************************/
+ *  Copyright by the contributors to the Dafny Project
+ *  SPDX-License-Identifier: MIT
+ *******************************************************************************/
 
 include "Interface.dfy"
 
diff --git a/src/Distributions/DiscreteLaplace/Interface.dfy b/src/Distributions/DiscreteLaplace/Interface.dfy
index 6520125e..99092226 100644
--- a/src/Distributions/DiscreteLaplace/Interface.dfy
+++ b/src/Distributions/DiscreteLaplace/Interface.dfy
@@ -1,7 +1,7 @@
 /*******************************************************************************
-*  Copyright by the contributors to the Dafny Project
-*  SPDX-License-Identifier: MIT
-*******************************************************************************/
+ *  Copyright by the contributors to the Dafny Project
+ *  SPDX-License-Identifier: MIT
+ *******************************************************************************/
 
 include "../Bernoulli/Interface.dfy"
 include "../Uniform/Interface.dfy"
diff --git a/src/Distributions/Geometric/Correctness.dfy b/src/Distributions/Geometric/Correctness.dfy
index 01f8e315..8fa837a8 100644
--- a/src/Distributions/Geometric/Correctness.dfy
+++ b/src/Distributions/Geometric/Correctness.dfy
@@ -1,7 +1,7 @@
 /*******************************************************************************
-*  Copyright by the contributors to the Dafny Project
-*  SPDX-License-Identifier: MIT
-*******************************************************************************/
+ *  Copyright by the contributors to the Dafny Project
+ *  SPDX-License-Identifier: MIT
+ *******************************************************************************/
 
 include "../../Math/Helper.dfy"
 include "../../ProbabilisticProgramming/Monad.dfy"
@@ -20,7 +20,7 @@ module GeometricCorrectness {
   /*******
    Lemmas
   *******/
-  
+
   // Equation (4.19)
   lemma {:axiom} ProbGeometricIsIndepFn()
     ensures Independence.IsIndepFn(GeometricModel.ProbGeometric())
diff --git a/src/Distributions/Geometric/Implementation.dfy b/src/Distributions/Geometric/Implementation.dfy
index 772f225c..55184afb 100644
--- a/src/Distributions/Geometric/Implementation.dfy
+++ b/src/Distributions/Geometric/Implementation.dfy
@@ -1,7 +1,7 @@
 /*******************************************************************************
-*  Copyright by the contributors to the Dafny Project
-*  SPDX-License-Identifier: MIT
-*******************************************************************************/
+ *  Copyright by the contributors to the Dafny Project
+ *  SPDX-License-Identifier: MIT
+ *******************************************************************************/
 
 include "../../ProbabilisticProgramming/Monad.dfy"
 include "Interface.dfy"
diff --git a/src/Distributions/Geometric/Interface.dfy b/src/Distributions/Geometric/Interface.dfy
index 3ce96882..32ee6619 100644
--- a/src/Distributions/Geometric/Interface.dfy
+++ b/src/Distributions/Geometric/Interface.dfy
@@ -1,7 +1,7 @@
 /*******************************************************************************
-*  Copyright by the contributors to the Dafny Project
-*  SPDX-License-Identifier: MIT
-*******************************************************************************/
+ *  Copyright by the contributors to the Dafny Project
+ *  SPDX-License-Identifier: MIT
+ *******************************************************************************/
 
 include "../../ProbabilisticProgramming/Monad.dfy"
 include "../Base/Interface.dfy"
diff --git a/src/Distributions/Geometric/Model.dfy b/src/Distributions/Geometric/Model.dfy
index d0e2b3a5..e15c8cc6 100644
--- a/src/Distributions/Geometric/Model.dfy
+++ b/src/Distributions/Geometric/Model.dfy
@@ -1,7 +1,7 @@
 /*******************************************************************************
-*  Copyright by the contributors to the Dafny Project
-*  SPDX-License-Identifier: MIT
-*******************************************************************************/
+ *  Copyright by the contributors to the Dafny Project
+ *  SPDX-License-Identifier: MIT
+ *******************************************************************************/
 
 include "../../ProbabilisticProgramming/Monad.dfy"
 include "../../ProbabilisticProgramming/WhileAndUntil.dfy"
@@ -19,7 +19,7 @@ module GeometricModel {
     Monad.Bind(g, f)
   }
 
-    // Equation (4.17)
+  // Equation (4.17)
   function ProbGeometricIter(t: (bool, int)): (f: Monad.Hurd<(bool, int)>)
     ensures forall s :: f(s) == ((Monad.Head(s), t.1 + 1), Monad.Tail(s))
   {
diff --git a/src/Distributions/Uniform/Implementation.dfy b/src/Distributions/Uniform/Implementation.dfy
index 457848a4..e51b3310 100644
--- a/src/Distributions/Uniform/Implementation.dfy
+++ b/src/Distributions/Uniform/Implementation.dfy
@@ -1,7 +1,7 @@
 /*******************************************************************************
-*  Copyright by the contributors to the Dafny Project
-*  SPDX-License-Identifier: MIT
-*******************************************************************************/
+ *  Copyright by the contributors to the Dafny Project
+ *  SPDX-License-Identifier: MIT
+ *******************************************************************************/
 
 include "../UniformPowerOfTwo/Interface.dfy"
 include "../UniformPowerOfTwo/Implementation.dfy"
diff --git a/src/Distributions/Uniform/Interface.dfy b/src/Distributions/Uniform/Interface.dfy
index 1c083605..2ab201fd 100644
--- a/src/Distributions/Uniform/Interface.dfy
+++ b/src/Distributions/Uniform/Interface.dfy
@@ -1,7 +1,7 @@
 /*******************************************************************************
-*  Copyright by the contributors to the Dafny Project
-*  SPDX-License-Identifier: MIT
-*******************************************************************************/
+ *  Copyright by the contributors to the Dafny Project
+ *  SPDX-License-Identifier: MIT
+ *******************************************************************************/
 
 include "../Base/Interface.dfy"
 include "../UniformPowerOfTwo/Interface.dfy"
diff --git a/src/Distributions/Uniform/Model.dfy b/src/Distributions/Uniform/Model.dfy
index 149ed9a6..c9c171f1 100644
--- a/src/Distributions/Uniform/Model.dfy
+++ b/src/Distributions/Uniform/Model.dfy
@@ -1,7 +1,7 @@
 /*******************************************************************************
-*  Copyright by the contributors to the Dafny Project
-*  SPDX-License-Identifier: MIT
-*******************************************************************************/
+ *  Copyright by the contributors to the Dafny Project
+ *  SPDX-License-Identifier: MIT
+ *******************************************************************************/
 
 include "../../ProbabilisticProgramming/RandomNumberGenerator.dfy"
 include "../../ProbabilisticProgramming/Monad.dfy"
diff --git a/src/Distributions/UniformPowerOfTwo/Correctness.dfy b/src/Distributions/UniformPowerOfTwo/Correctness.dfy
index 1e00dbbb..9f2ee5aa 100644
--- a/src/Distributions/UniformPowerOfTwo/Correctness.dfy
+++ b/src/Distributions/UniformPowerOfTwo/Correctness.dfy
@@ -196,38 +196,38 @@ module UniformPowerOfTwoCorrectness {
     ensures UnifIsCorrect(n, 1, m)
   {
     calc {
+      RandomNumberGenerator.mu(iset s | UniformPowerOfTwoModel.ProbUnif(n)(s).0 == m);
+    == { ProbUnifCaseSplit(n, m); }
+      RandomNumberGenerator.mu(iset s | 2*UniformPowerOfTwoModel.ProbUnif(n / 2)(s).0 + 1 == m) / 2.0;
+    == { assert (iset s | 2*UniformPowerOfTwoModel.ProbUnif(n / 2)(s).0 + 1 == m) == (iset s {:trigger 1 == m} | 1 == m); }
+      RandomNumberGenerator.mu(iset s {:trigger 1 == m} | 1 == m) / 2.0;
+    }
+    if m < Helper.Power(2, 1) {
+      assert m == 1;
+      calc {
         RandomNumberGenerator.mu(iset s | UniformPowerOfTwoModel.ProbUnif(n)(s).0 == m);
-      == { ProbUnifCaseSplit(n, m); }
-        RandomNumberGenerator.mu(iset s | 2*UniformPowerOfTwoModel.ProbUnif(n / 2)(s).0 + 1 == m) / 2.0;
-      == { assert (iset s | 2*UniformPowerOfTwoModel.ProbUnif(n / 2)(s).0 + 1 == m) == (iset s {:trigger 1 == m} | 1 == m); }
+      ==
         RandomNumberGenerator.mu(iset s {:trigger 1 == m} | 1 == m) / 2.0;
+      == { assert (iset s: RandomNumberGenerator.RNG {:trigger 1 == m} | 1 == m) == (iset s {:trigger true} | true); }
+        RandomNumberGenerator.mu(iset s {:trigger true} | true) / 2.0;
+      == { RandomNumberGenerator.RNGHasMeasure(); Helper.DivisionSubstituteAlternativeReal(2.0, RandomNumberGenerator.mu(iset s {:trigger true} | true), 1.0); }
+        1.0 / 2.0;
+      ==
+        1.0 / (Helper.Power(2, 1) as real);
+      }
+    } else {
+      assert m != 1;
+      calc {
+        RandomNumberGenerator.mu(iset s: RandomNumberGenerator.RNG | UniformPowerOfTwoModel.ProbUnif(n)(s).0 == m);
+      ==
+        RandomNumberGenerator.mu(iset s: RandomNumberGenerator.RNG {:trigger 1 == m} | 1 == m) / 2.0;
+      == { assert (iset s: RandomNumberGenerator.RNG {:trigger 1 == m} | 1 == m) == iset{}; }
+        RandomNumberGenerator.mu(iset {}) / 2.0;
+      == { RandomNumberGenerator.RNGHasMeasure(); }
+        0.0 / 2.0;
+      ==
+        0.0;
       }
-      if m < Helper.Power(2, 1) {
-        assert m == 1;
-        calc {
-          RandomNumberGenerator.mu(iset s | UniformPowerOfTwoModel.ProbUnif(n)(s).0 == m);
-        ==
-          RandomNumberGenerator.mu(iset s {:trigger 1 == m} | 1 == m) / 2.0;
-        == { assert (iset s: RandomNumberGenerator.RNG {:trigger 1 == m} | 1 == m) == (iset s {:trigger true} | true); }
-          RandomNumberGenerator.mu(iset s {:trigger true} | true) / 2.0;
-        == { RandomNumberGenerator.RNGHasMeasure(); Helper.DivisionSubstituteAlternativeReal(2.0, RandomNumberGenerator.mu(iset s {:trigger true} | true), 1.0); }
-          1.0 / 2.0;
-        ==
-          1.0 / (Helper.Power(2, 1) as real);
-        }
-      } else {
-        assert m != 1;
-        calc {
-          RandomNumberGenerator.mu(iset s: RandomNumberGenerator.RNG | UniformPowerOfTwoModel.ProbUnif(n)(s).0 == m);
-        ==
-          RandomNumberGenerator.mu(iset s: RandomNumberGenerator.RNG {:trigger 1 == m} | 1 == m) / 2.0;
-        == { assert (iset s: RandomNumberGenerator.RNG {:trigger 1 == m} | 1 == m) == iset{}; }
-          RandomNumberGenerator.mu(iset {}) / 2.0;
-        == { RandomNumberGenerator.RNGHasMeasure(); }
-          0.0 / 2.0;
-        ==
-          0.0;
-        }
     }
   }
 
@@ -315,13 +315,13 @@ module UniformPowerOfTwoCorrectness {
     ensures (1.0 / Helper.Power(2, k) as real) / 2.0 == 1.0 / (Helper.Power(2, k + 1) as real)
   {
     calc {
-        (1.0 / Helper.Power(2, k) as real) / 2.0;
-      == { Helper.DivDivToDivMul(1.0, Helper.Power(2, k) as real, 2.0); }
-        1.0 / (Helper.Power(2, k) as real * 2.0);
-      == { Helper.NatMulNatToReal(Helper.Power(2, k), 2); }
-        1.0 / (Helper.Power(2, k) * 2) as real;
-      ==
-        1.0 / (Helper.Power(2, k + 1) as real);
+      (1.0 / Helper.Power(2, k) as real) / 2.0;
+    == { Helper.DivDivToDivMul(1.0, Helper.Power(2, k) as real, 2.0); }
+      1.0 / (Helper.Power(2, k) as real * 2.0);
+    == { Helper.NatMulNatToReal(Helper.Power(2, k), 2); }
+      1.0 / (Helper.Power(2, k) * 2) as real;
+    ==
+      1.0 / (Helper.Power(2, k + 1) as real);
     }
   }
 
@@ -366,13 +366,13 @@ module UniformPowerOfTwoCorrectness {
             forall s ensures f(s) in e <==> g(s) in e' {
               calc {
                 f(s) in e;
-                <==> { assert f(s) == UniformPowerOfTwoModel.ProbUnif(n)(s).1; }
+              <==> { assert f(s) == UniformPowerOfTwoModel.ProbUnif(n)(s).1; }
                 UniformPowerOfTwoModel.ProbUnif(n)(s).1 in e;
-                <==> { ProbUnifTailDecompose(n, s); }
+              <==> { ProbUnifTailDecompose(n, s); }
                 Monad.Tail(UniformPowerOfTwoModel.ProbUnif(n / 2)(s).1) in e;
-                <==>
+              <==>
                 UniformPowerOfTwoModel.ProbUnif(n / 2)(s).1 in e';
-                <==> { assert UniformPowerOfTwoModel.ProbUnif(n / 2)(s).1 == g(s); }
+              <==> { assert UniformPowerOfTwoModel.ProbUnif(n / 2)(s).1 == g(s); }
                 g(s) in e';
               }
             }
diff --git a/src/Distributions/UniformPowerOfTwo/Implementation.dfy b/src/Distributions/UniformPowerOfTwo/Implementation.dfy
index 69f15771..a82f88a7 100644
--- a/src/Distributions/UniformPowerOfTwo/Implementation.dfy
+++ b/src/Distributions/UniformPowerOfTwo/Implementation.dfy
@@ -1,7 +1,7 @@
 /*******************************************************************************
-*  Copyright by the contributors to the Dafny Project
-*  SPDX-License-Identifier: MIT
-*******************************************************************************/
+ *  Copyright by the contributors to the Dafny Project
+ *  SPDX-License-Identifier: MIT
+ *******************************************************************************/
 
 include "Interface.dfy"
 include "Model.dfy"
diff --git a/src/Distributions/UniformPowerOfTwo/Interface.dfy b/src/Distributions/UniformPowerOfTwo/Interface.dfy
index 60635558..936196ae 100644
--- a/src/Distributions/UniformPowerOfTwo/Interface.dfy
+++ b/src/Distributions/UniformPowerOfTwo/Interface.dfy
@@ -1,7 +1,7 @@
 /*******************************************************************************
-*  Copyright by the contributors to the Dafny Project
-*  SPDX-License-Identifier: MIT
-*******************************************************************************/
+ *  Copyright by the contributors to the Dafny Project
+ *  SPDX-License-Identifier: MIT
+ *******************************************************************************/
 
 include "../Base/Interface.dfy"
 include "Model.dfy"
diff --git a/src/Distributions/UniformPowerOfTwo/Model.dfy b/src/Distributions/UniformPowerOfTwo/Model.dfy
index 6a123240..6b68cb3f 100644
--- a/src/Distributions/UniformPowerOfTwo/Model.dfy
+++ b/src/Distributions/UniformPowerOfTwo/Model.dfy
@@ -1,7 +1,7 @@
 /*******************************************************************************
-*  Copyright by the contributors to the Dafny Project
-*  SPDX-License-Identifier: MIT
-*******************************************************************************/
+ *  Copyright by the contributors to the Dafny Project
+ *  SPDX-License-Identifier: MIT
+ *******************************************************************************/
 
 include "../../ProbabilisticProgramming/RandomNumberGenerator.dfy"
 include "../../ProbabilisticProgramming/Monad.dfy"
diff --git a/src/Math/Helper.dfy b/src/Math/Helper.dfy
index 274b979f..5f2504be 100644
--- a/src/Math/Helper.dfy
+++ b/src/Math/Helper.dfy
@@ -1,7 +1,7 @@
 /*******************************************************************************
-*  Copyright by the contributors to the Dafny Project
-*  SPDX-License-Identifier: MIT
-*******************************************************************************/
+ *  Copyright by the contributors to the Dafny Project
+ *  SPDX-License-Identifier: MIT
+ *******************************************************************************/
 
 module Helper {
   /************
@@ -107,9 +107,9 @@ module Helper {
   {
     calc {
       a * c + b;
-      ==
+    ==
       a * c + (a * (b / a) + b % a);
-      ==
+    ==
       a * (c + b / a) + b % a;
     }
     DivModIsUnique(a * c + b, a, c + b / a, b % a);
diff --git a/src/Math/MeasureTheory.dfy b/src/Math/MeasureTheory.dfy
index 89f76d35..bd9c168b 100644
--- a/src/Math/MeasureTheory.dfy
+++ b/src/Math/MeasureTheory.dfy
@@ -1,7 +1,7 @@
 /*******************************************************************************
-*  Copyright by the contributors to the Dafny Project
-*  SPDX-License-Identifier: MIT
-*******************************************************************************/
+ *  Copyright by the contributors to the Dafny Project
+ *  SPDX-License-Identifier: MIT
+ *******************************************************************************/
 
 module MeasureTheory {
   /************
@@ -21,7 +21,7 @@ module MeasureTheory {
     iset n: nat | n >= i, x <- f(n) :: x
   }
 
-  ghost function CountableSum(f: nat -> real, i: nat := 0): real {
+  function CountableSum(f: nat -> real, i: nat := 0): real {
     assume {:axiom} false;
     f(i) + CountableSum(f, i+1)
   }
@@ -71,7 +71,7 @@ module MeasureTheory {
   }
 
   // Definition 13
-  ghost predicate AreIndepEvents<T>(event_space: iset<iset<T>>, mu: iset<T> -> real, e1: iset<T>, e2: iset<T>) {
+  predicate AreIndepEvents<T>(event_space: iset<iset<T>>, mu: iset<T> -> real, e1: iset<T>, e2: iset<T>) {
     && (e1 in event_space)
     && (e2 in event_space)
     && (mu(e1 * e2) == mu(e1) * mu(e2))
@@ -107,13 +107,13 @@ module MeasureTheory {
         }
         calc {
           CountableSum((n: nat) => mu(f(n)))
-          ==
+       ==
           mu(f(0)) + CountableSum((n: nat) => mu(f(n)), 1)
-          ==
+       ==
           mu(f(0)) + mu(f(1)) + CountableSum((n: nat) => mu(f(n)), 2)
-          ==
+       ==
           mu(e1) + mu(e2) + CountableSum((n: nat) => mu(f(n)), 2)
-          ==
+       ==
           mu(e1) + mu(e2);
         }
       }
@@ -142,9 +142,9 @@ module MeasureTheory {
     assert CountableUnion(f) == e1 + e2 by {
       calc {
         CountableUnion(f);
-        == { CountableUnionSplit(f, 0); }
+      == { CountableUnionSplit(f, 0); }
         e1 + CountableUnion(f, 1);
-        == { CountableUnionSplit(f, 1); }
+      == { CountableUnionSplit(f, 1); }
         e1 + e2;
       }
     }
diff --git a/src/ProbabilisticProgramming/Independence.dfy b/src/ProbabilisticProgramming/Independence.dfy
index ccedfae5..9aa773d2 100644
--- a/src/ProbabilisticProgramming/Independence.dfy
+++ b/src/ProbabilisticProgramming/Independence.dfy
@@ -1,7 +1,7 @@
 /*******************************************************************************
-*  Copyright by the contributors to the Dafny Project
-*  SPDX-License-Identifier: MIT
-*******************************************************************************/
+ *  Copyright by the contributors to the Dafny Project
+ *  SPDX-License-Identifier: MIT
+ *******************************************************************************/
 
 include "RandomNumberGenerator.dfy"
 include "Monad.dfy"
@@ -29,7 +29,7 @@ module Independence {
   }
 
   // Definition 35
-  ghost predicate {:axiom} IsIndepFn<A>(f: Monad.Hurd<A>)
+  predicate {:axiom} IsIndepFn<A>(f: Monad.Hurd<A>)
     ensures IsIndepFunction(f)
     ensures MeasureTheory.IsMeasurable(RandomNumberGenerator.event_space, RandomNumberGenerator.event_space, s => f(s).1)
 
diff --git a/src/ProbabilisticProgramming/Quantifier.dfy b/src/ProbabilisticProgramming/Quantifier.dfy
index 4062b335..80aa5254 100644
--- a/src/ProbabilisticProgramming/Quantifier.dfy
+++ b/src/ProbabilisticProgramming/Quantifier.dfy
@@ -1,7 +1,7 @@
 /*******************************************************************************
-*  Copyright by the contributors to the Dafny Project
-*  SPDX-License-Identifier: MIT
-*******************************************************************************/
+ *  Copyright by the contributors to the Dafny Project
+ *  SPDX-License-Identifier: MIT
+ *******************************************************************************/
 
 include "RandomNumberGenerator.dfy"
 
diff --git a/src/ProbabilisticProgramming/RandomNumberGenerator.dfy b/src/ProbabilisticProgramming/RandomNumberGenerator.dfy
index a57a8eb1..4ab3b098 100644
--- a/src/ProbabilisticProgramming/RandomNumberGenerator.dfy
+++ b/src/ProbabilisticProgramming/RandomNumberGenerator.dfy
@@ -1,7 +1,7 @@
 /*******************************************************************************
-*  Copyright by the contributors to the Dafny Project
-*  SPDX-License-Identifier: MIT
-*******************************************************************************/
+ *  Copyright by the contributors to the Dafny Project
+ *  SPDX-License-Identifier: MIT
+ *******************************************************************************/
 
 include "../Math/MeasureTheory.dfy"
 
diff --git a/src/ProbabilisticProgramming/WhileAndUntil.dfy b/src/ProbabilisticProgramming/WhileAndUntil.dfy
index 2426e21e..167cb436 100644
--- a/src/ProbabilisticProgramming/WhileAndUntil.dfy
+++ b/src/ProbabilisticProgramming/WhileAndUntil.dfy
@@ -1,7 +1,7 @@
 /*******************************************************************************
-*  Copyright by the contributors to the Dafny Project
-*  SPDX-License-Identifier: MIT
-*******************************************************************************/
+ *  Copyright by the contributors to the Dafny Project
+ *  SPDX-License-Identifier: MIT
+ *******************************************************************************/
 
 include "Monad.dfy"
 include "Quantifier.dfy"
@@ -32,8 +32,8 @@ module WhileAndUntil {
 
   // Definition 39 / True iff mu(iset s | ProbWhile(c, b, a)(s) terminates) == 1
   ghost predicate ProbWhileTerminates<A(!new)>(b: A -> Monad.Hurd<A>, c: A -> bool) {
-    var P := (a: A) => 
-      (s: RandomNumberGenerator.RNG) => exists n :: !c(ProbWhileCut(c, b, n, a)(s).0);
+    var P := (a: A) =>
+               (s: RandomNumberGenerator.RNG) => exists n :: !c(ProbWhileCut(c, b, n, a)(s).0);
     forall a :: Quantifier.ForAllStar(P(a))
   }
 
@@ -48,12 +48,12 @@ module WhileAndUntil {
       Monad.Return(a)
   }
 
-  method ProbWhileImperative<A>(c: A -> bool, b: A -> Monad.Hurd<A>, a: A, s: RandomNumberGenerator.RNG) returns (t: (A, RandomNumberGenerator.RNG)) 
+  method ProbWhileImperative<A>(c: A -> bool, b: A -> Monad.Hurd<A>, a: A, s: RandomNumberGenerator.RNG) returns (t: (A, RandomNumberGenerator.RNG))
     requires ProbWhileTerminates(b, c)
     ensures ProbWhile(c, b, a)(s) == t
     decreases *
   {
-    while c(a) 
+    while c(a)
       decreases *
     {
       var (a, s) := b(a)(s);
@@ -61,7 +61,7 @@ module WhileAndUntil {
     return (a, s);
   }
 
-  method ProbWhileImperativeAlternative<A>(c: A -> bool, b: A -> Monad.Hurd<A>, a: A, s: RandomNumberGenerator.RNG) returns (t: (A, RandomNumberGenerator.RNG)) 
+  method ProbWhileImperativeAlternative<A>(c: A -> bool, b: A -> Monad.Hurd<A>, a: A, s: RandomNumberGenerator.RNG) returns (t: (A, RandomNumberGenerator.RNG))
     requires ProbWhileTerminates(b, c)
     ensures ProbWhile(c, b, a)(s) == t
     decreases *
@@ -86,7 +86,7 @@ module WhileAndUntil {
   // Definition 44
   function ProbUntil<A>(b: Monad.Hurd<A>, c: A -> bool): (f: Monad.Hurd<A>)
     requires ProbUntilTerminates(b, c)
-    ensures 
+    ensures
       var c' := (a: A) => !c(a);
       var b' := (a: A) => b;
       forall s :: f(s) == ProbWhile(c', b', b(s).0)(b(s).1)
diff --git a/tests/Tests.dfy b/tests/Tests.dfy
index 5308cb96..18e25d42 100644
--- a/tests/Tests.dfy
+++ b/tests/Tests.dfy
@@ -3,9 +3,9 @@
  *  SPDX-License-Identifier: MIT
  *******************************************************************************/
 
- include "../src/Dafny-VMC.dfy"
+include "../src/Dafny-VMC.dfy"
 
- module Tests {
+module Tests {
   import BaseInterface
   import UniformInterface
   import GeometricInterface
@@ -267,4 +267,4 @@
     var varianceBound := 1.4 * 1.4; // variance of DiscreteGaussian(1.4) is < 1.4^2
     testEmpiricalIsWithin4SigmaOfTrueMean(n, sum as real, 0.0, varianceBound, "mean");
   }
- }
+}
diff --git a/tests/TestsExternUniform.dfy b/tests/TestsExternUniform.dfy
index 54bb2c41..8770f80a 100644
--- a/tests/TestsExternUniform.dfy
+++ b/tests/TestsExternUniform.dfy
@@ -3,8 +3,8 @@
  *  SPDX-License-Identifier: MIT
  *******************************************************************************/
 
- include "../src/Dafny-VMC.dfy"
- include "Tests.dfy"
+include "../src/Dafny-VMC.dfy"
+include "Tests.dfy"
 
 module TestsExternUniform {
   import DafnyVMC
@@ -48,14 +48,14 @@ module TestsExternUniform {
   {
     var r := new DafnyVMC.DRandomExternUniform();
     Tests.TestBernoulliRational2(1_000_000, r);
-  }  
+  }
 
   method {:test} TestBernoulliRational3()
     decreases *
   {
     var r := new DafnyVMC.DRandomExternUniform();
     Tests.TestBernoulliRational3(1_000_000, r);
-  }  
+  }
 
   method {:test} TestBernoulli()
     decreases *
diff --git a/tests/TestsFoundational.dfy b/tests/TestsFoundational.dfy
index 5c09ffee..0c2cf3f6 100644
--- a/tests/TestsFoundational.dfy
+++ b/tests/TestsFoundational.dfy
@@ -3,8 +3,8 @@
  *  SPDX-License-Identifier: MIT
  *******************************************************************************/
 
- include "../src/Dafny-VMC.dfy"
- include "Tests.dfy"
+include "../src/Dafny-VMC.dfy"
+include "Tests.dfy"
 
 module TestsFoundational {
   import DafnyVMC
@@ -48,14 +48,14 @@ module TestsFoundational {
   {
     var r := new DafnyVMC.DRandomFoundational();
     Tests.TestBernoulliRational2(1_000_000, r);
-  }  
+  }
 
   method {:test} TestBernoulliRational3()
     decreases *
   {
     var r := new DafnyVMC.DRandomFoundational();
     Tests.TestBernoulliRational3(1_000_000, r);
-  }  
+  }
 
   method {:test} TestBernoulli()
     decreases *