a draft signature and test for zippers

You can check that if you comment out the `balance` call in the
`close` function, the property will fail.

There are two problems with this first try at testing RBT zippers:

- I cannot say that when a (foo option) actually returns a (Some v),
  we can populate (foo) with (v). So I had to lift everything at the
  level of (foo option). I think we may need to add constructors for
  products and sums at either the Ty or Fn level.

- The current implementation is *very* slow on this example. It feels
  like it is exponential in the number of operations of the signature.
add a cutoff to element generation to terminate on large signatures