Let type checker discharge `fin (blocks x y)` and `fin (padding x y)`.
Let type checker discharge `fin (blocks x y)` and `fin (padding x y)`.

Both of these type operators are always either finite or undefined.

GaloisInc/cryptol,GaloisInc/cryptol,GaloisInc/cryptol