<pre><code>ω (\h \lst. (isempty lst) zero (add one ((h h) (extract-tail lst))))
</code></pre>
+
and this will indeed implement the recursive function we couldn't earlier figure out how to define.
In broad brush-strokes, `H` is half of the `get_length` function we're seeking, and `H` has the form: