When I was attempting to prove Bloom's original incorrect bound, the work never progressed to the point where I was actively working directly on proving his bou

When I was attempting to prove Bloom's original incorrect bound, the work never progressed to the point where I was actively working directly on proving his bound - I managed to prove some intermediate theorems, but was unable to work out a way to compose them. The issue ended up being that that I was unable to derive the independence required to prove the inductive step. If you're interested at looking at the sources, I think the following commit was around the place where I was working on this: https://github.com/certichain/ceramist/commit/70927c5b50e21a08f510cfd9555d8324a61c1233 https://github.com/certichain/ceramist/commit/70927c5b50e21a...