diff --git a/src/Distributions/BernoulliExpNeg/Implementation.dfy b/src/Distributions/BernoulliExpNeg/Implementation.dfy
index 75bd0796..d504ceb6 100644
--- a/src/Distributions/BernoulliExpNeg/Implementation.dfy
+++ b/src/Distributions/BernoulliExpNeg/Implementation.dfy
@@ -29,8 +29,11 @@ module BernoulliExpNeg.Implementation {
         invariant gamma'.numer >= 0
         invariant Model.GammaReductionLoop((true, gamma))(old(s)) == Model.GammaReductionLoop((b, gamma'))(s)
       {
+        var prevGamma := gamma';
+        var prevS := s;
         b := BernoulliExpNegSampleCaseLe1(Rationals.Int(1));
         gamma' := Rationals.Rational(gamma'.numer - gamma'.denom, gamma'.denom);
+        assert Model.GammaReductionLoop((true, prevGamma))(prevS) == Model.GammaReductionLoop((b, gamma'))(s);
       }
       if b {
         c:= BernoulliExpNegSampleCaseLe1(gamma');