Doesn't compile, unfinished.

The idea is to make an abstraction over "statements",
such that they are either done by a recursive proof verification
or by doing some minor logic in-circuit.

For the action state extension statement, it would be
short-circuiting if source and target are only N actions
from each other (for e.g. N = 8), but more than that
could use a recursive proof (and reusing the portion of the
circuit to verify the last N ones).

Then, we can define short-circuiting proof composition,
currently called WrapTwo dumbly,
such that if either of the two wrapped statements can be short-circuited,
then we avoid an extra proof.

This is very useful for reducing proofs to deal with the 2 recursive proof
verifications per circuit limit, since you can stack WrapTwos on top of WrapTwos,
and only proving when necessary, short-circuiting the rest.

Closes #162