chiark / gitweb /
strategy: move traversal proofs inline