Recursive proofs
----------------

TODO