Rework bounded proofs

Now the rewrite strategy no longer relies on projections of anything
other than [decode], and the conversion to ZLike is simpler.

Modulo some annoyingly delicate arithmetic around things like [2^n * 2^n
= 2^(2*n)] and whether to factor [(decode (fst x) + decode (snd x) >> n)
>> b] as [decode x >> n] or as [shrd (fst x) (snd x) n], the proofs
bascially go by pulling/pushing decodes.

0 files changed, 0 insertions, 0 deletions